Problem (2008USAMOp2): Let $ ABC$ be an acute, scalene triangle, and let $ M$, $ N$, and $ P$ be the midpoints of $ \overline{BC}$, $ \overline{CA}$, and $ \overline{AB}$, respectively. Let the perpendicular bisectors of $ \overline{AB}$ and $ \overline{AC}$ intersect ray $ AM$ in points $ D$ and $ E$ respectively, and let lines $ BD$ and $ CE$ intersect in point $ F$, inside of triangle $ ABC$. Prove that points $ A$, $ N$, $ F$, and $ P$ all lie on one circle.
AlphaGeometry formalization: a b c = triangle; m = midpoint b c; n = midpoint c a; p = midpoint a b; d = on_bline a b, on_line a m; e = on_bline a c, on_line a m; f = on_line b d, on_line c e ? cyclic a n f p
HAGeo formalization: A B C = acute_triangle; M = midpoint B C; N = midpoint C A; P = midpoint A B; AB = line A B; l1 = perpendicular_bisector A B; AM = line A M; D = intersection l1 AM; AC = line A C; l2 = perpendicular_bisector A C; E = intersection l2 AM; BD = line B D; CE = line C E; F = intersection BD CE; Prove: concyclic A N F P
Difficulty score: 3.0