Problem (ShuZhiMiGeo180): Let $D,E,F$ be contact points of $\triangle ABC$'s excircles. Points $X,Y,Z,U,V,W$ satisfy $DY=DW=EZ=EU=FX=FV$. If $O_1,\dots,O_6$ are circumcenters of $\triangle AUV,\triangle BVW,\triangle CWU,\triangle AZX,\triangle BXY,\triangle CYZ$ respectively, then line $IO$ (where $I,O$ are incenter and circumcenter) is the radical axis of $\triangle O_1O_2O_3$ and $\triangle O_4O_5O_6$'s circumcircles
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; o = circumcenter a b c; i_a = excenter a b c; d = foot i_a b c; i_b = excenter b c a; e = foot i_b a c; i_c = excenter c a b; f = foot i_c a b; u = on_line a c; z = mirror u e; v = on_line a b, eqdistance v f e u; x = mirror v f; w = on_line b c, eqdistance w d u e; y = mirror w d; o1 = circumcenter a u v; o2 = circumcenter b v w; o3 = circumcenter c w u; o4 = circumcenter a z x; o5 = circumcenter b x y; o6 = circumcenter c y z; oa = circumcenter o1 o2 o3; ob = circumcenter o4 o5 o6; t = on_circle oa o1, on_circle ob o4 ? coll i o t
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; AC = line A C; AB = line A B; O = circumcenter A B C; Ia = excenter A B C; D = foot Ia BC; Ib = excenter B C A; E = foot Ib AC; I_c = excenter C A B; F = foot I_c AB; U = on_line AC; Z = reflect_point_wrt_point U E; AB = line A B; (F) = circle_center_radius F E U; V = intersection AB (F); X = reflect_point_wrt_point V F; BC = line B C; (D) = circle_center_radius D E U; W = intersection BC (D); Y = reflect_point_wrt_point W D; O1 = circumcenter A U V; O2 = circumcenter B V W; O3 = circumcenter C W U; O4 = circumcenter A Z X; O5 = circumcenter B X Y; O6 = circumcenter C Y Z; Oa = circumcenter O1 O2 O3; Ob = circumcenter O4 O5 O6; (Oa) = circle_center_point Oa O1; (Ob) = circle_center_point Ob O4; T = intersection (Oa) (Ob); Prove: collinear I O T
Difficulty score: 5.3