Problem (2024TurkeyTSTp9): In a scalene triangle $ABC,$ $I$ is the incenter and $O$ is the circumcenter. The line $IO$ intersects the lines $BC,CA,AB$ at points $D,E,F$ respectively. Let $A_1$ be the intersection of $BE$ and $CF$. The points $B_1$ and $C_1$ are defined similarly. The incircle of $ABC$ is tangent to sides $BC,CA,AB$ at points $X,Y,Z$ respectively. Let the lines $XA_1, YB_1$ and $ZC_1$ intersect $IO$ at points $A_2,B_2,C_2$ respectively. Prove that the circles with diameters $AA_2,BB_2$ and $CC_2$ have a common point.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; o = circumcenter a b c; d = on_line i o, on_line b c; e = on_line i o, on_line a c; f = on_line i o, on_line a b; a1 = on_line b e, on_line c f; b1 = on_line c f, on_line a d; c1 = on_line a d, on_line b e; x = foot i b c; y = foot i a c; z = foot i a b; a2 = on_line x a1, on_line i o; b2 = on_line y b1, on_line i o; c2 = on_line z c1, on_line i o; k = on_dia a a2, on_dia b b2 ? perp c k k c2
HAGeo formalization: A B C = triangle; I = incenter A B C; O = circumcenter A B C; IO = line I O; BC = line B C; D = intersection IO BC; AC = line A C; E = intersection IO AC; AB = line A B; F = intersection IO AB; BE = line B E; CF = line C F; A1 = intersection BE CF; AD = line A D; B1 = intersection CF AD; C1 = intersection AD BE; X = foot I BC; Y = foot I AC; Z = foot I AB; XA1 = line X A1; A2 = intersection XA1 IO; YB1 = line Y B1; B2 = intersection YB1 IO; ZC1 = line Z C1; C2 = intersection ZC1 IO; (AA2) = circle_diameter A A2; (BB2) = circle_diameter B B2; K = intersection (AA2) (BB2); CK = line C K; C2K = line C2 K; Prove: perpendicular CK C2K
Difficulty score: 5.9