Problem (2025CTSTp8): Let quadrilateral $A_1A_2A_3A_4$ be not cyclic and haves edges not parallel to each other. Denote $B_i$ as the intersection of the tangent line at $A_i$ with respect to circle $A_{i-1}A_iA_{i+1}$ and the $A_{i+2}$-symmedian with respect to triangle $A_{i+1}A_{i+2}A_{i+3}$ and $C_i$ as the intersection of lines $A_iA_{i+1}$ and $B_iB_{i+1}$, where all indexes taken cyclically. Prove that $C_1$, $C_2$, $C_3$, and $C_4$ are collinear.
AlphaGeometry formalization: a1 a2 a3 a4 = quadrangle; o1 = circumcenter a4 a1 a2; o2 = circumcenter a1 a2 a3; o3 = circumcenter a2 a3 a4; o4 = circumcenter a3 a4 a1; m1 = midpoint a1 a3; m2 = midpoint a2 a4; b1 = on_tline a1 o1 a1, on_aline b1 a3 a2 a4 a3 m2; b2 = on_tline a2 o2 a2, on_aline b2 a4 a3 a1 a4 m1; b3 = on_tline a3 o3 a3, on_aline b3 a1 a4 a2 a1 m2; b4 = on_tline a4 o4 a4, on_aline b4 a2 a1 a3 a2 m1; c1 = on_line a1 a2, on_line b1 b2; c2 = on_line a2 a3, on_line b2 b3; c3 = on_line a3 a4, on_line b3 b4 ? coll c1 c2 c3
HAGeo formalization: A1 A2 A3 A4 = quadrilateral; O1 = circumcenter A4 A1 A2; O2 = circumcenter A1 A2 A3; O3 = circumcenter A2 A3 A4; O4 = circumcenter A3 A4 A1; M1 = midpoint A1 A3; M2 = midpoint A2 A4; O1A1 = line O1 A1; O2A2 = line O2 A2; O3A3 = line O3 A3; O4A4 = line O4 A4; l1 = perpendicular_line A1 O1A1; l2 = perpendicular_line A2 O2A2; l3 = perpendicular_line A3 O3A3; l4 = perpendicular_line A4 O4A4; m1 = angle_equal1 A3 A2 A4 A3 M2; m2 = angle_equal1 A4 A3 A1 A4 M1; m3 = angle_equal1 A1 A4 A2 A1 M2; m4 = angle_equal1 A2 A1 A3 A2 M1; B1 = intersection l1 m1; B2 = intersection l2 m2; B3 = intersection l3 m3; B4 = intersection l4 m4; A1A2 = line A1 A2; B1B2 = line B1 B2; C1 = intersection A1A2 B1B2; A2A3 = line A2 A3; B2B3 = line B2 B3; C2 = intersection A2A3 B2B3; A3A4 = line A3 A4; B3B4 = line B3 B4; C3 = intersection A3A4 B3B4; Prove: collinear C1 C2 C3
Difficulty score: 6.3