Problem (2024KoMaLA864): Let $ABC$ be a triangle and $O$ be its circumcenter. Let $D$, $E$ and $F$ be the respective tangent points of the incircle of $\triangle ABC$, and sides $BC$, $CA$ and $AB$. Let $M$ and $N$ be the respective midpoints of sides $AB$ and $AC$. Let $M'$ and $N'$ be the respective reflections of points $M$ and $N$ across lines $DE$ and $DF$. Let lines $CM'$ and $BN'$ intersect lines $DE$ and $DF$ at points $H$ and $J$, respectively. Prove that the points $H$, $J$ and $O$ are collinear.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; i = incenter a b c; d = foot i b c; e = foot i a c; f = foot i a b; m = midpoint a b; n = midpoint a c; m1 = reflect m d e; n1 = reflect n d f; h = on_line c m1, on_line d e; j = on_line b n1, on_line d f ? coll h j o
HAGeo formalization: A B C = triangle; O = circumcenter A B C; I = incenter A B C; BC = line B C; D = foot I BC; AC = line A C; E = foot I AC; AB = line A B; F = foot I AB; M = midpoint A B; N = midpoint A C; DE = line D E; M1 = reflect_point_wrt_line M DE; DF = line D F; N1 = reflect_point_wrt_line N DF; CM1 = line C M1; H = intersection CM1 DE; BN1 = line B N1; J = intersection BN1 DF; Prove: collinear H J O
Difficulty score: 5.6