Problem (ShuZhiMiGeo635): Let $\triangle ABC$ have incircle $\odot I$ tangent to $BC,CA,AB$ at $D,E,F$ respectively, with $AD,BE,CF$ meeting at $K$. Lines $AK,BK,CK$ meet the circumcircle again at $X,Y,Z$. If $O_A,O_B,O_C$ are circumcenters of $\triangle YKZ,\triangle ZKX,\triangle XKY$ respectively, prove that the centroid $G$ of $\triangle O_AO_BO_C$ lies on line $IK$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; d = foot i b c; e = foot i a c; f = foot i a b; k = on_line a d, on_line b e; o = circumcenter a b c; x = on_line a k, on_circle o a; y = on_line b k, on_circle o a; z = on_line c k, on_circle o a; oa = circumcenter y k z; ob = circumcenter z k x; oc = circumcenter x k y; m1 m2 m3 g = centroid oa ob oc ? coll g i k
HAGeo formalization: A B C = triangle; I = incenter A B C; BC = line B C; AC = line A C; AB = line A B; D = foot I BC; E = foot I AC; F = foot I AB; AD = line A D; BE = line B E; K = intersection AD BE; O = circumcenter A B C; AK = line A K; (O) = circle_center_point O A; X = intersection AK (O); BK = line B K; Y = intersection BK (O); CK = line C K; Z = intersection CK (O); Oa = circumcenter Y K Z; Ob = circumcenter Z K X; Oc = circumcenter X K Y; G M1 M2 M3 = centroid Oa Ob Oc; Prove: collinear G I K
Difficulty score: 5.0