Problem (2006G9): Points $ A_{1}$, $ B_{1}$, $ C_{1}$ are chosen on the sides $ BC$, $ CA$, $ AB$ of a triangle $ ABC$ respectively. The circumcircles of triangles $ AB_{1}C_{1}$, $ BC_{1}A_{1}$, $ CA_{1}B_{1}$ intersect the circumcircle of triangle $ ABC$ again at points $ A_{2}$, $ B_{2}$, $ C_{2}$ respectively ($ A_{2}\neq A, B_{2}\neq B, C_{2}\neq C$). Points $ A_{3}$, $ B_{3}$, $ C_{3}$ are symmetric to $ A_{1}$, $ B_{1}$, $ C_{1}$ with respect to the midpoints of the sides $ BC$, $ CA$, $ AB$ respectively. Prove that the triangles $ A_{2}B_{2}C_{2}$ and $ A_{3}B_{3}C_{3}$ are similar.
AlphaGeometry formalization: a b c = triangle; a1 = on_line b c; b1 = on_line a c; c1 = on_line a b; o = circumcenter a b c; o1 = circumcenter a b1 c1; a2 = on_circle o1 a, on_circle o a; o2 = circumcenter b c1 a1; b2 = on_circle o2 b, on_circle o b; o3 = circumcenter c a1 b1; c2 = on_circle o3 c, on_circle o c; m1 = midpoint b c; a3 = mirror a1 m1; m2 = midpoint a c; b3 = mirror b1 m2; m3 = midpoint a b; c3 = mirror c1 m3 ? simtri a2 b2 c2 a3 b3 c3
HAGeo formalization: A B C = triangle; BC = line B C; A1 = on_line BC; AC = line A C; B1 = on_line AC; AB = line A B; C1 = on_line AB; O = circumcenter A B C; (ABC) = circle_center_point O A; O1 = circumcenter A B1 C1; (AB1C1) = circle_center_point O1 A; A2 = intersection (ABC) (AB1C1); O2 = circumcenter B C1 A1; (A1BC1) = circle_center_point O2 B; B2 = intersection (ABC) (A1BC1); O3 = circumcenter C A1 B1; (A1B1C) = circle_center_point O3 C; C2 = intersection (ABC) (A1B1C); L = midpoint B C; A3 = reflect A1 L; M = midpoint C A; B3 = reflect B1 M; N = midpoint A B; C3 = reflect C1 N; Prove: similar A2 B2 C2 A3 B3 C3
Difficulty score: 3.2