Problem (2005CTSTp19): Convex quadrilateral $ABCD$ is cyclic in circle $(O)$, $P$ is the intersection of the diagonals $AC$ and $BD$. Circle $(O_{1})$ passes through $P$ and $B$, circle $(O_{2})$ passes through $P$ and $A$, Circles $(O_{1})$ and $(O_{2})$ intersect at $P$ and $Q$. $(O_{1})$, $(O_{2})$ intersect $(O)$ at another points $E$, $F$ (besides $B$, $A$), respectively. Prove that $PQ$, $CE$, $DF$ are concurrent or parallel.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; o = circumcenter a b c; p = on_line a c, on_line b d; o1 = on_bline p b; o2 = on_bline p a; q = on_circle o1 p, on_circle o2 p; e = on_circle o1 p, on_circle o a; f = on_circle o2 p, on_circle o a; x = on_line p q, on_line c e ? coll x d f
HAGeo formalization: A B C = triangle; O = circumcenter A B C; (O) = circle_center_point O A; D = on_circle (O); AC = line A C; BD = line B D; P = intersection AC BD; l1 = perpendicular_bisector P B; O1 = on_line l1; (O1) = circle_center_point O1 P; l2 = perpendicular_bisector P A; O2 = on_line l2; (O2) = circle_center_point O2 P; Q = intersection (O1) (O2); E = intersection (O1) (O); F = intersection (O2) (O); PQ = line P Q; CE = line C E; DF = line D F; X = intersection PQ CE; Prove: collinear X D F
Difficulty score: 2.9