Problem (2007USATSTp1): Circles $ \omega_1$ and $ \omega_2$ meet at $ P$ and $ Q$. Segments $ AC$ and $ BD$ are chords of $ \omega_1$ and $ \omega_2$ respectively, such that segment $ AB$ and ray $ CD$ meet at $ P$. Ray $ BD$ and segment $ AC$ meet at $ X$. Point $ Y$ lies on $ \omega_1$ such that $ PY \parallel BD$. Point $ Z$ lies on $ \omega_2$ such that $ PZ \parallel AC$. Prove that points $ Q,X,Y,Z$ are collinear.
AlphaGeometry formalization: p q = segment; o1 = on_bline p q; o2 = on_bline p q; a = on_circle o1 p; b = on_line a p, on_circle o2 q; d = on_circle o2 q; c = on_line p d, on_circle o1 p; x = on_line b d, on_line a c; y = on_circle o1 p, on_pline p b d ? coll q x y
HAGeo formalization: P = point; Q = point; l = perpendicular_bisector P Q; O1 = on_line l; O2 = on_line l; (O1) = circle_center_point O1 P; (O2) = circle_center_point O2 P; A = on_circle (O1); C = on_circle (O1); AP = line A P; B = intersection (O2) AP; CP = line C P; D = intersection (O2) CP; AC = line A C; BD = line B D; X = intersection AC BD; l1 = parallel_line P BD; Y = intersection (O1) l1; Prove: collinear Q X Y
Difficulty score: 2.1