Problem (ShuZhiMiGeo256): In acute $\triangle ABC$ with circumcenter $O$ and symmedian point $K$, let $X,Y,Z$ be the nine-point centers of $\triangle BOC,\triangle COA,\triangle AOB$ respectively, and $G_e$ be the Gergonne point of $\triangle XYZ$. Prove $O,G_e,K$ are collinear with $OG_e=3G_eK$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; m1 m2 m3 g = centroid a b c; k = on_aline k a b c a g, on_aline k b a c b g; ma = midpoint o a; mb = midpoint o b; mc = midpoint o c; x = circumcenter m1 mb mc; y = circumcenter m2 ma mc; z = circumcenter m3 ma mb; i = incenter x y z; d = foot i y z; e = foot i x z; ge = on_line x d, on_line y e; n = midpoint o k ? midp ge n k
HAGeo formalization: A B C = triangle; O = circumcenter A B C; G M1 M2 M3 = centroid A B C; l1 = angle_equal1 A B C A G; l2 = angle_equal1 B A C B G; K = intersection l1 l2; Ma = midpoint O A; Mb = midpoint O B; Mc = midpoint O C; X = circumcenter M1 Mb Mc; Y = circumcenter M2 Ma Mc; Z = circumcenter M3 Ma Mb; I = incenter X Y Z; YZ = line Y Z; XZ = line X Z; D = foot I YZ; E = foot I XZ; XD = line X D; YE = line Y E; Ge = intersection XD YE; N = midpoint O K; Prove: midpoint Ge N K
Difficulty score: 6.5