Problem (2006CGMOp2): Let $O$ be the intersection of the diagonals of convex quadrilateral $ABCD$. The circumcircles of $\triangle{OAD}$ and $\triangle{OBC}$ meet at $O$ and $M$. Line $OM$ meets the circumcircles of $\triangle{OAB}$ and $\triangle{OCD}$ at $T$ and $S$ respectively. Prove that $M$ is the midpoint of $ST$.
AlphaGeometry formalization: a b c d = quadrangle; o = on_line a c, on_line b d; o1 = circumcenter o a d; o2 = circumcenter o b c; m = on_circle o1 o, on_circle o2 o; o3 = circumcenter o a b; t = on_line o m, on_circle o3 o; o4 = circumcenter o c d; s = on_line o m, on_circle o4 o ? midp m s t
HAGeo formalization: A B C D = quadrilateral; AC = line A C; BD = line B D; O = intersection AC BD; (ADO) = circle A D O; (BCO) = circle B C O; M = intersection (ADO) (BCO); MO = line M O; (ABO) = circle A B O; T = intersection MO (ABO); (CDO) = circle C D O; S = intersection MO (CDO); Prove: midpoint M S T
Difficulty score: 2.3