Problem (2019IranTSTp15): In triangle $ABC$, $M,N$ and $P$ are midpoints of sides $BC,CA$ and $AB$. Point $K$ lies on segment $NP$ so that $AK$ bisects $\angle BKC$. Lines $MN,BK$ intersects at $E$ and lines $MP,CK$ intersects at $F$. Suppose that $H$ be the foot of perpendicular line from $A$ to $BC$ and $L$ the second intersection of circumcircle of triangles $AKH, HEF$. Prove that $MK,EF$ and $HL$ are concurrent.
AlphaGeometry formalization: k b c = triangle; b1 = mirror b k; c1 = mirror c k; a = on_line b1 c1, angle_bisector b k c; m = midpoint b c; n = midpoint c a; p = midpoint a b; e = on_line m n, on_line b k; f = on_line m p, on_line c k; h = foot a b c; o1 = circumcenter a k h; o2 = circumcenter h e f; l = on_circle o1 a, on_circle o2 h; x = on_line m k, on_line e f ? coll x h l
HAGeo formalization: K B C = triangle; B1 = reflect_point_wrt_point B K; C1 = reflect_point_wrt_point C K; B1C1 = line B1 C1; l1 = angle_bisector B K C; A = intersection B1C1 l1; M = midpoint B C; N = midpoint C A; P = midpoint A B; MN = line M N; BK = line B K; E = intersection MN BK; MP = line M P; CK = line C K; F = intersection MP CK; BC = line B C; H = foot A BC; O1 = circumcenter A K H; O2 = circumcenter H E F; (O1) = circle_center_point O1 A; (O2) = circle_center_point O2 H; L = intersection (O1) (O2); MK = line M K; EF = line E F; X = intersection MK EF; Prove: collinear X H L
Difficulty score: 4.1