Problem (ShuZhiMiGeo309): In $\triangle ABC$, let $\omega_1,\omega_2,\omega_3$ be A/B/C-excircles with contact points $A_i,B_i,C_i$ on sides. Lines $A_1A_2,B_1B_2,C_1C_2$ form $\triangle DEF$ with circumcircle $\Omega$. Let $X,Y,Z$ be radical centers of ($\Omega,\omega_2,\omega_3$), ($\Omega,\omega_3,\omega_1$), ($\Omega,\omega_1,\omega_2$). If $O_1,O_2$ are circumcenters of $\triangle DEF,\triangle XYZ$, prove $I$ lies on $O_1O_2$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; i1 = excenter a b c; i2 = excenter b c a; i3 = excenter c a b; a1 = foot i1 a b; a2 = foot i1 a c; b1 = foot i2 b c; b2 = foot i2 b a; c1 = foot i3 c a; c2 = foot i3 c b; d = on_line b1 b2, on_line c1 c2; e = on_line a1 a2, on_line c1 c2; f = on_line a1 a2, on_line b1 b2; o1 = circumcenter d e f; x1 = on_circle o1 d, on_circle i1 a1; x2 = on_circle o1 d, on_circle i1 a1; y1 = on_circle o1 d, on_circle i2 b1; y2 = on_circle o1 d, on_circle i2 b1; z1 = on_circle o1 d, on_circle i3 c1; z2 = on_circle o1 d, on_circle i3 c1; x = on_line y1 y2, on_line z1 z2; y = on_line x1 x2, on_line z1 z2; z = on_line x1 x2, on_line y1 y2; o2 = circumcenter x y z ? coll i o1 o2
HAGeo formalization: A B C = triangle; I = incenter A B C; I1 = excenter A B C; I2 = excenter B C A; I3 = excenter C A B; BC = line B C; AC = line C A; AB = line A B; A1 = foot I1 AB; A2 = foot I1 AC; B1 = foot I2 BC; B2 = foot I2 AB; C1 = foot I3 AC; C2 = foot I3 BC; B1B2 = line B1 B2; C1C2 = line C1 C2; D = intersection B1B2 C1C2; A1A2 = line A1 A2; E = intersection A1A2 C1C2; F = intersection A1A2 B1B2; O1 = circumcenter D E F; (O1) = circle_center_point O1 D; (I1) = circle_center_point I1 A1; X1 X2 = intersection (O1) (I1); (I2) = circle_center_point I2 B1; Y1 Y2 = intersection (O1) (I2); (I3) = circle_center_point I3 C1; Z1 Z2 = intersection (O1) (I3); Y1Y2 = line Y1 Y2; Z1Z2 = line Z1 Z2; X = intersection Y1Y2 Z1Z2; X1X2 = line X1 X2; Y = intersection X1X2 Z1Z2; Z = intersection X1X2 Y1Y2; O2 = circumcenter X Y Z; Prove: collinear I O1 O2
Difficulty score: 6.1