Problem (2010AsiaPacificMOp4): Let $ABC$ be an acute angled triangle satisfying the conditions $AB>BC$ and $AC>BC$. Denote by $O$ and $H$ the circumcentre and orthocentre, respectively, of the triangle $ABC.$ Suppose that the circumcircle of the triangle $AHC$ intersects the line $AB$ at $M$ different from $A$, and the circumcircle of the triangle $AHB$ intersects the line $AC$ at $N$ different from $A.$ Prove that the circumcentre of the triangle $MNH$ lies on the line $OH$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; o1 = circumcenter a h c; m = on_line a b, on_circle o1 a; o2 = circumcenter a h b; n = on_line a c, on_circle o2 a; o3 = circumcenter m n h ? coll o3 o h
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; H = orthocenter A B C; AB = line A B; O1 = circumcenter A C H; (O1) = circle_center_point O1 A; M = intersection AB (O1); AC = line A C; O2 = circumcenter A B H; (O2) = circle_center_point O2 A; N = intersection AC (O2); P = circumcenter M N H; Prove: collinear P H O
Difficulty score: 3.0