Problem (2019CzechAPSlovakp6): Let $ABC$ be an acute triangle with $AB<AC$ and $\angle BAC=60^{\circ}$. Denote its altitudes by $AD,BE,CF$ and its orthocenter by $H$. Let $K,L,M$ be the midpoints of sides $BC,CA,AB$, respectively. Prove that the midpoints of segments $AH, DK, EL, FM$ lie on a single circle.
AlphaGeometry formalization: a b x = ieq_triangle; c = on_line a x; d = foot a b c; e = foot b a c; f = foot c a b; h = orthocenter a b c; k = midpoint b c; l = midpoint c a; m = midpoint a b; p1 = midpoint a h; p2 = midpoint d k; p3 = midpoint e l; p4 = midpoint f m ? cyclic p1 p2 p3 p4
HAGeo formalization: A B X = equilateral_triangle; AX = line A X; C = on_line AX; BC = line B C; AC = line A C; AB = line A B; D = foot A BC; E = foot B AC; F = foot C AB; H = orthocenter A B C; K = midpoint B C; L = midpoint C A; M = midpoint A B; P1 = midpoint A H; P2 = midpoint D K; P3 = midpoint E L; P4 = midpoint F M; Prove: concyclic P1 P2 P3 P4
Difficulty score: 4.3