Problem (ShuZhiMiGeo117): In $\triangle ABC$ with circumcenter $O$, incenter $I$, and A-excenter $I_A$, let $BI\cap AC=E$, $CI\cap AB=F$, and $K$ be the isogonal conjugate of $I$ wrt $\triangle I_AEF$. If $X$ is $K$'s projection on $EF$, prove $OI$ bisects $KX$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; i = incenter a b c; ia = excenter a b c; e = on_line b i, on_line a c; f = on_line c i, on_line a b; k = on_aline k f e ia f i, on_aline k e f ia e i; x = foot k e f; m = midpoint k x ? coll m o i
HAGeo formalization: A B C = triangle; O = circumcenter A B C; I = incenter A B C; Ia = excenter A B C; BI = line B I; AC = line A C; E = intersection BI AC; CI = line C I; AB = line A B; F = intersection CI AB; l1 = angle_equal1 F E Ia F I; l2 = angle_equal1 E F Ia E I; K = intersection l1 l2; EF = line E F; X = foot K EF; M = midpoint K X; Prove: collinear M O I
Difficulty score: 6.4