Problem (2005USAMOp3): Let $ABC$ be an acute-angled triangle, and let $P$ and $Q$ be two points on its side $BC$. Construct a point $C_{1}$ in such a way that the convex quadrilateral $APBC_{1}$ is cyclic, $QC_{1}\parallel CA$, and $C_{1}$ and $Q$ lie on opposite sides of line $AB$. Construct a point $B_{1}$ in such a way that the convex quadrilateral $APCB_{1}$ is cyclic, $QB_{1}\parallel BA$, and $B_{1}$ and $Q$ lie on opposite sides of line $AC$. Prove that the points $B_{1}$, $C_{1}$, $P$, and $Q$ lie on a circle.
AlphaGeometry formalization: a b c = triangle; p = on_line b c; q = on_line b c; c1 = on_circum a p b, on_pline q c a; b1 = on_circum a p c, on_pline q b a ? cyclic b1 c1 p q
HAGeo formalization: A B C = acute_triangle; BC = line B C; P = on_line BC; Q = on_line BC; AC = line A C; l1 = parallel_line Q AC; (ABP) = circle A B P; C1 = intersection (ABP) l1; AB = line A B; l2 = parallel_line Q AB; (ACP) = circle A C P; B1 = intersection (ACP) l2; Prove: concyclic B1 C1 P Q
Difficulty score: 1.8