Problem (2007CMOp4): Let $O, I$ be the circumcenter and incenter of triangle $ABC$. The incircle of $\triangle ABC$ touches $BC, CA, AB$ at points $D, E, F$ repsectively. $FD$ meets $CA$ at $P$, $ED$ meets $AB$ at $Q$. $M$ and $N$ are midpoints of $PE$ and $QF$ respectively. Show that $OI \perp MN$.
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; p = on_line f d, on_line a c; q = on_line e d, on_line a b; m = midpoint p e; n = midpoint q f ? perp o i m n
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; DF = line D F; P = intersection DF AC; DE = line D E; Q = intersection DE AB; M = midpoint P E; N = midpoint Q F; IO = line I O; MN = line M N; Prove: perpendicular IO MN
Difficulty score: 2.1