Problem (2021CHNGaoLianA2): As shown in the figure, in the acute angle $\vartriangle ABC$, $AB > AC$, $M$ is the midpoint of the minor arc $BC$ of the circumcircle $\Omega$ of $\vartriangle ABC$. $K$ is the intersection point of the bisector of the exterior angle $\angle BAC$ and the extension line of $BC$. From point $A$ draw a line perpendicular on $BC$ and take a point $D$ (different from $A$) on that line , such that $DM = AM$. Let the circumscribed circle of $\vartriangle ADK$ intersect the circle $\Omega$ at point $A$ and at another point $T$. Prove that $AT$ bisects line segment $BC$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; m = on_circum a b c, on_bline b c; x = angle_bisector b a c; k = on_tline a a x, on_line b c; d = on_tline a b c, on_circle m a; o2 = circumcenter a d k; t = on_circle o2 a, on_circum a b c; n = midpoint b c ? coll a t n
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; (O) = circle_center_point O A; M = midarc_no B C A; l1 = angle_exbisector B A C; BC = line B C; K = intersection l1 BC; l2 = perpendicular_line A BC; (M) = circle_center_point M A; D = intersection l2 (M); O2 = circumcenter A D K; (O2) = circle_center_point O2 A; T = intersection (O2) (O); N = midpoint B C; Prove: collinear A T N
Difficulty score: 2.7