Problem (2024ARMOg9p6): The altitudes of an acute triangle $ABC$ with $AB<AC$ intersect at a point $H$, and $O$ is the center of the circumcircle $\Omega$. The segment $OH$ intersects the circumcircle of $BHC$ at a point $X$, different from $O$ and $H$. The circumcircle of $AOX$ intersects the smaller arc $AB$ of $\Omega$ at point $Y$. Prove that the line $XY$ bisects the segment $BC$.
AlphaGeometry formalization: a b c = triangle; h = orthocenter a b c; o = circumcenter a b c; o1 = circumcenter b h c; x = on_line o h, on_circle o1 b; o2 = circumcenter a o x; y = on_circle o a, on_circle o2 a; m = midpoint b c ? coll x y m
HAGeo formalization: A B C = acute_triangle; H = orthocenter A B C; O = circumcenter A B C; (O) = circle_center_point O A; HO = line H O; O1 = circumcenter B C H; (O1) = circle_center_point O1 B; X = intersection HO (O1); O2 = circumcenter A O X; (O2) = circle_center_point O2 A; Y = intersection (O2) (O); XY = line X Y; BC = line B C; M = midpoint B C; Prove: collinear M X Y
Difficulty score: 3.0