Problem (2017IranGOAp3): Let $O$ be the circumcenter of triangle $ABC$. Line $CO$ intersects the altitude from $A$ at point $K$. Let $P,M$ be the midpoints of $AK$, $AC$ respectively. If $PO$ intersects $BC$ at $Y$, and the circumcircle of triangle $BCM$ meets $AB$ at $X$, prove that $BXOY$ is cyclic.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; k = on_line c o, on_tline a b c; p = midpoint a k; m = midpoint a c; y = on_line b c, on_line p o; o1 = circumcenter b c m; x = on_line a b, on_circle o1 b ? cyclic b x o y
HAGeo formalization: A B C = triangle; O = circumcenter A B C; BC = line B C; l1 = perpendicular_line A BC; CO = line C O; K = intersection CO l1; P = midpoint A K; M = midpoint A C; OP = line O P; Y = intersection OP BC; AB = line A B; O1 = circumcenter B C M; (BCM) = circle_center_point O1 B; X = intersection AB (BCM); Prove: concyclic B X O Y
Difficulty score: 3.2