Problem (2023IMOp6): Let $ABC$ be an equilateral triangle. Let $A_1,B_1,C_1$ be interior points of $ABC$ such that $BA_1=A_1C$, $CB_1=B_1A$, $AC_1=C_1B$, and $$\angle BA_1C+\angle CB_1A+\angle AC_1B=480^\circ$$Let $BC_1$ and $CB_1$ meet at $A_2,$ let $CA_1$ and $AC_1$ meet at $B_2,$ and let $AB_1$ and $BA_1$ meet at $C_2.$ Prove that if triangle $A_1B_1C_1$ is scalene, then the three circumcircles of triangles $AA_1A_2, BB_1B_2$ and $CC_1C_2$ all pass through two common points.
AlphaGeometry formalization: a b c = ieq_triangle; o = circumcenter a b c; a1 = on_bline b c; b1 = on_bline c a; c0 = on_aline c0 a b a1 c b1; c1 = on_bline a b, on_aline c1 a b c0 a o; a2 = on_line b c1, on_line c b1; b2 = on_line c a1, on_line a c1; c2 = on_line a b1, on_line b a1; o1 = circumcenter a a1 a2; o2 = circumcenter b b1 b2; o3 = circumcenter c c1 c2; x = on_circle o1 a, on_circle o2 b ? cyclic x c c1 c2
HAGeo formalization: A B C = equilateral_triangle; O = circumcenter A B C; l1 = perpendicular_bisector B C; A1 = on_line l1; l2 = perpendicular_bisector A C; B1 = on_line l2; l3 = perpendicular_bisector A B; l4 = angle_equal1 A B A1 C B1; C0 = on_line l4; l5 = angle_equal1 A B C0 A O; C1 = intersection l3 l5; BC1 = line B C1; CB1 = line C B1; A2 = intersection BC1 CB1; CA1 = line C A1; AC1 = line A C1; B2 = intersection CA1 AC1; AB1 = line A B1; BA1 = line B A1; C2 = intersection AB1 BA1; O1 = circumcenter A A1 A2; O2 = circumcenter B B1 B2; O3 = circumcenter C C1 C2; (O1) = circle_center_point O1 A; (O2) = circle_center_point O2 B; X = intersection (O1) (O2); Prove: concyclic X C C1 C2
Difficulty score: 6.4