Problem (2024ShuZhiMiMOM4p6): In $\triangle ABC$ with incircle $(I)$ tangent to $AB,AC$ at $F,E$, line $EF$ meets $(ABC)$ at $P,Q$. Let $BI,CI$ meet $(IPQ)$ again at $L,K$, and the external bisector of $\angle BAC$ meet $(ABC)$ at $N$ and the Euler line at $M$. Prove $K,L,M,N$ are concyclic.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; f = foot i a b; e = foot i a c; o = circumcenter a b c; p = on_line e f, on_circle o a; q = on_line e f, on_circle o a; o1 = circumcenter i p q; l = on_line b i, on_circle o1 i; k = on_line c i, on_circle o1 i; n = on_tline a a i, on_circle o a; h = orthocenter a b c; m = on_tline a a i, on_line o h ? cyclic k l m n
HAGeo formalization: A B C = triangle; I = incenter A B C; AC = line A C; AB = line A B; F = foot I AB; E = foot I AC; O = circumcenter A B C; EF = line E F; (O) = circle_center_point O A; P = intersection EF (O); Q = intersection EF (O); O1 = circumcenter I P Q; BI = line B I; (O1) = circle_center_point O1 I; L = intersection BI (O1); CI = line C I; K = intersection CI (O1); AI = line A I; l1 = perpendicular_line A AI; N = intersection l1 (O); H = orthocenter A B C; OH = line O H; M = intersection l1 OH; Prove: concyclic K L M N
Difficulty score: 6.0