Problem (2023USAMOp1): In an acute triangle $ABC$, let $M$ be the midpoint of $\overline{BC}$. Let $P$ be the foot of the perpendicular from $C$ to $AM$. Suppose that the circumcircle of triangle $ABP$ intersects line $BC$ at two distinct points $B$ and $Q$. Let $N$ be the midpoint of $\overline{AQ}$. Prove that $NB=NC$.
AlphaGeometry formalization: a b c = triangle; m = midpoint b c; p = foot c a m; q = on_line b c, on_circum a b p; n = midpoint a q ? cong n b n c
HAGeo formalization: A B C = acute_triangle; M = midpoint B C; AM = line A M; P = foot C AM; (ABP) = circle A B P; BC = line B C; Q = intersection (ABP) BC; N = midpoint A Q; Prove: cong B N C N
Difficulty score: 1.7