Problem (2019CHNWesternMOp5): In acute-angled triangle $ABC,$ $AB>AC.$ Let $O,H$ be the circumcenter and orthocenter of $\triangle ABC,$ respectively. The line passing through $H$ and parallel to $AB$ intersects line $AC$ at $M,$ and the line passing through $H$ and parallel to $AC$ intersects line $AB$ at $N.$ $L$ is the reflection of the point $H$ in $MN.$ Line $OL$ and $AH$ intersect at $K.$ Prove that $K,M,L,N$ are concyclic.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; m = on_pline h a b, on_line a c; n = on_pline h a c, on_line a b; l = reflect h m n; k = on_line o l, on_line a h ? cyclic k m l n
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; H = orthocenter A B C; AB = line A B; l1 = parallel_line H AB; AC = line A C; M = intersection l1 AC; l2 = parallel_line H AC; N = intersection l2 AB; MN = line M N; L = reflect_point_wrt_line H MN; LO = line L O; AH = line A H; K = intersection LO AH; Prove: concyclic K M L N
Difficulty score: 2.9