Problem (2010CTSTp19): Given acute triangle $ABC$ with $AB>AC$, let $M$ be the midpoint of $BC$. $P$ is a point in triangle $AMC$ such that $\angle MAB=\angle PAC$. Let $O,O_1,O_2$ be the circumcenters of $\triangle ABC,\triangle ABP,\triangle ACP$ respectively. Prove that line $AO$ passes through the midpoint of $O_1 O_2$.
AlphaGeometry formalization: a b c = triangle; m = midpoint b c; p = on_aline p a c b a m; o = circumcenter a b c; o1 = circumcenter a b p; o2 = circumcenter a c p; n = midpoint o1 o2 ? coll a o n
HAGeo formalization: A B C = acute_triangle; M = midpoint B C; l1 = angle_equal1 A C B A M; P = on_line l1; O = circumcenter A B C; O1 = circumcenter A B P; O2 = circumcenter A C P; N = midpoint O1 O2; Prove: collinear A O N
Difficulty score: 2.2