Problem (2017AsiaPacificMOp2): Let $ABC$ be a triangle with $AB < AC$. Let $D$ be the intersection point of the internal bisector of angle $BAC$ and the circumcircle of $ABC$. Let $Z$ be the intersection point of the perpendicular bisector of $AC$ with the external bisector of angle $\angle{BAC}$. Prove that the midpoint of the segment $AB$ lies on the circumcircle of triangle $ADZ$.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c, angle_bisector b a c; z = on_tline a a d, on_bline a c; n = midpoint a b ? cyclic a d z n
HAGeo formalization: A B C = triangle; l1 = angle_bisector B A C; (ABC) = circle A B C; D = intersection (ABC) l1; l2 = perpendicular_bisector A C; l3 = angle_exbisector B A C; Z = intersection l2 l3; N = midpoint A B; Prove: concyclic A D Z N
Difficulty score: 2.1