Problem (2013G2): Let $\omega$ be the circumcircle of a triangle $ABC$. Denote by $M$ and $N$ the midpoints of the sides $AB$ and $AC$, respectively, and denote by $T$ the midpoint of the arc $BC$ of $\omega$ not containing $A$. The circumcircles of the triangles $AMT$ and $ANT$ intersect the perpendicular bisectors of $AC$ and $AB$ at points $X$ and $Y$, respectively; assume that $X$ and $Y$ lie inside the triangle $ABC$. The lines $MN$ and $XY$ intersect at $K$. Prove that $KA=KT$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; m = midpoint a b; n = midpoint a c; t = on_circle o a, angle_bisector b a c; o1 = circumcenter a m t; o2 = circumcenter a n t; x = on_circle o1 a, on_bline a c; y = on_circle o2 a, on_bline a b; k = on_line m n, on_line x y ? cong k a k t
HAGeo formalization: A B C = triangle; O = circumcenter A B C; M = midpoint A B; N = midpoint A C; l1 = angle_bisector B A C; (ABC) = circle_center_point O A; T = intersection l1 (ABC); l2 = perpendicular_bisector A C; O1 = circumcenter A M T; (AMT) = circle_center_point O1 A; X = intersection (AMT) l2; l3 = perpendicular_bisector A B; O2 = circumcenter A N T; (ANT) = circle_center_point O2 A; Y = intersection (ANT) l3; MN = line M N; XY = line X Y; K = intersection MN XY; Prove: cong K A K T
Difficulty score: 3.0