Problem (2017USAMOp3): Let $ABC$ be a scalene triangle with circumcircle $\Omega$ and incenter $I$. Ray $AI$ meets $\overline{BC}$ at $D$ and meets $\Omega$ again at $M$; the circle with diameter $\overline{DM}$ cuts $\Omega$ again at $K$. Lines $MK$ and $BC$ meet at $S$, and $N$ is the midpoint of $\overline{IS}$. The circumcircles of $\triangle KID$ and $\triangle MAN$ intersect at points $L_1$ and $L_2$. Prove that $\Omega$ passes through the midpoint of either $\overline{IL_1}$ or $\overline{IL_2}$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; i = incenter a b c; d = on_line a i, on_line b c; m = on_line a i, on_circle o a; k = on_dia m d, on_circle o a; s = on_line m k, on_line b c; n = midpoint i s; o1 = circumcenter k i d; o2 = circumcenter m a n; l = on_circle o1 k, on_circle o2 m; p = midpoint i l ? cyclic a b c p
HAGeo formalization: A B C = triangle; I = incenter A B C; AI = line A I; BC = line B C; D = intersection AI BC; O = circumcenter A B C; (O) = circle_center_point O A; M = intersection AI (O); (DM) = circle_diameter D M; K = intersection (DM) (O); KM = line K M; S = intersection KM BC; N = midpoint I S; O1 = circumcenter D I K; (O1) = circle_center_point O1 K; O2 = circumcenter A M N; (O2) = circle_center_point O2 M; L = intersection (O1) (O2); P = midpoint I L; Prove: concyclic A B C P
Difficulty score: 3.8