Problem (2012CHNGaoLian): In an acute-angled triangle $ABC$, $AB>AC$. $M,N$ are distinct points on side $BC$ such that $\angle BAM=\angle CAN$. Let $O_1,O_2$ be the circumcentres of $\triangle ABC, \triangle AMN$, respectively. Prove that $O_1,O_2,A$ are collinear.
AlphaGeometry formalization: a b c = triangle; m = on_line b c; n = on_line b c, on_aline n a c b a m; o1 = circumcenter a b c; o2 = circumcenter a m n ? coll o1 o2 a
HAGeo formalization: A B C = acute_triangle; BC = line B C; M = on_line BC; l = angle_equal1 A C B A M; N = intersection BC l; O1 = circumcenter A B C; O2 = circumcenter A M N; Prove: collinear O1 O2 A
Difficulty score: 1.7