Problem (2020CSMGOp2): Let $\triangle ABC$ be a triangle with the incenter $I$, and circumcircle $\omega$. Let the circle with diameter $AI$ intersect $\omega$ at a point $S\ne A$. Let $M$ be the midpoint of the arc $\widehat{BAC}$ and let $MI$ intersect $\omega$ again at a point $T\ne M$. Let the circumcircle of $\triangle MIS$ intersect the circumcircle of $\triangle BIC$ at a point $X\ne I$. Let the tangent at $S$ to $\omega$ intersect $BC$ at a point $V$. Prove that $MX$ and $VT$ intersect on $\omega$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; o = circumcenter a b c; m1 = midpoint a i; s = on_circle m1 a, on_circle o a; m = on_bline b c, on_circle o a; t = on_line m i, on_circle o a; o1 = circumcenter m i s; o2 = circumcenter b i c; x = on_circle o1 m, on_circle o2 b; v = on_tline s o s, on_line b c; y = on_line m x, on_line v t ? cyclic y a b c
HAGeo formalization: A B C = triangle; I = incenter A B C; O = circumcenter A B C; M1 = midpoint A I; (M1) = circle_center_point M1 A; (O) = circle_center_point O A; S = intersection (M1) (O); l1 = perpendicular_bisector B C; M = intersection l1 (O); IM = line I M; T = intersection IM (O); O1 = circumcenter I M S; O2 = circumcenter B C I; (O1) = circle_center_point O1 M; (O2) = circle_center_point O2 B; X = intersection (O1) (O2); OS = line O S; l2 = perpendicular_line S OS; BC = line B C; V = intersection l2 BC; MX = line M X; TV = line T V; Y = intersection MX TV; Prove: concyclic Y A B C
Difficulty score: 3.7