Problem (2022CTSTp1): In a cyclic convex hexagon $ABCDEF$, $AB$ and $DC$ intersect at $G$, $AF$ and $DE$ intersect at $H$. Let $M, N$ be the circumcenters of $BCG$ and $EFH$, respectively. Prove that the $BE$, $CF$ and $MN$ are concurrent.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_circle o a; e = on_circle o a; f = on_circle o a; g = on_line a b, on_line d c; h = on_line a f, on_line d e; m = circumcenter b c g; n = circumcenter e f h; x = on_line b e, on_line c f ? coll m n x
HAGeo formalization: A B C = triangle; O = circumcenter A B C; (O) = circle_center_point O A; D = on_circle (O); E = on_circle (O); F = on_circle (O); AB = line A B; CD = line C D; G = intersection AB CD; AF = line A F; DE = line D E; H = intersection AF DE; M = circumcenter B C G; N = circumcenter E F H; BE = line B E; CF = line C F; X = intersection BE CF; Prove: collinear M N X
Difficulty score: 2.8