Problem (2023KoMaLA855): In scalene triangle $ABC$ the shortest side is $BC$. Let points $M$ and $N$ be chosen on sides $AB$ and $AC$, respectively, such that $BM=CN=BC$. Let $I$ and $O$ denote the incenter and circumcentre of triangle $ABC$, and let $D$ and $E$ denote the incenter and circumcenter of triangle $AMN$. Prove that lines $IO$ and $DE$ intersect each other on the circumcircle of triangle $ABC$.
AlphaGeometry formalization: a b c = triangle; m = on_line a b, eqdistance m b c b; n = on_line a c, eqdistance n c c b; i = incenter a b c; o = circumcenter a b c; d = incenter a m n; e = circumcenter a m n; x = on_line i o, on_line d e ? cyclic x a b c
HAGeo formalization: A B C = triangle; AB = line A B; (B,BC) = circle_center_radius B B C; M = intersection AB (B,BC); AC = line A C; (C,BC) = circle_center_radius C B C; N = intersection AC (C,BC); I = incenter A B C; O = circumcenter A B C; D = incenter A M N; E = circumcenter A M N; IO = line I O; DE = line D E; X = intersection IO DE; Prove: concyclic X A B C
Difficulty score: 4.7