Problem (2015EuropeanMCupSp3): Circles $k_1$ and $k_2$ intersect in points $A$ and $B$, such that $k_1$ passes through the center $O$ of the circle $k_2$. The line $p$ intersects $k_1$ in points $K$ and $O$ and $k_2$ in points $L$ and $M$, such that the point $L$ is between $K$ and $O$. The point $P$ is orthogonal projection of the point $L$ to the line $AB$. Prove that the line $KP$ is parallel to the $M-$median of the triangle $ABM$.
AlphaGeometry formalization: a b = segment; o = on_bline a b; t = free; k = on_line o t, on_circum a b o; l = on_line o t, on_circle o a; m = mirror l o; p = foot l a b; n = midpoint a b ? para k p m n
HAGeo formalization: A = point; B = point; l = perpendicular_bisector A B; O = on_line l; (ABO) = circumcircle A B O; K = on_circle (ABO); OK = line O K; (O) = circle_center_point O A; L M = intersection OK (O); AB = line A B; P = foot L AB; N = midpoint A B; KP = line K P; MN = line M N; Prove: parallel KP MN
Difficulty score: 1.7