Problem (2023IranGOAp4): Let $ABC$ be a triangle with bisectors $BE$ and $CF$ meet at $I$. Let $D$ be the projection of $I$ on the $BC$. Let M and $N$ be the orthocenters of triangles $AIF$ and $AIE$, respectively. Lines $EM$ and $FN$ meet at $P.$ Let $X$ be the midpoint of $BC$. Let $Y$ be the point lying on the line $AD$ such that $XY \perp IP$. Prove that line $AI$ bisects the segment $XY$.
AlphaGeometry formalization: a b c = triangle; e = on_line a c, angle_bisector a b c; f = on_line a b, angle_bisector a c b; i = incenter a b c; d = foot i b c; m = orthocenter a i f; n = orthocenter a i e; p = on_line e m, on_line f n; x = midpoint b c; y = on_line a d, on_tline x i p; m_xy = midpoint x y ? coll m_xy a i
HAGeo formalization: A B C = triangle; l1 = angle_bisector A B C; AC = line A C; E = intersection l1 AC; l2 = angle_bisector B C A; AB = line A B; F = intersection l2 AB; I = incenter A B C; BC = line B C; D = foot I BC; M = orthocenter A I F; N = orthocenter A I E; EM = line E M; FN = line F N; P = intersection EM FN; X = midpoint B C; IP = line I P; l3 = perpendicular_line X IP; AD = line A D; Y = intersection AD l3; L = midpoint X Y; Prove: collinear L A I
Difficulty score: 5.1