Problem (2021CGMOp2): In acute triangle $ABC$ ($AB \neq AC$), $I$ is its incenter and $J$ is the $A$-excenter. $X, Y$ are on minor arcs $\widehat{AB}$ and $\widehat{AC}$ respectively such that $\angle{AXI}=\angle{AYJ}=90^{\circ}$. $K$ is on line $BC$ such that $KI=KJ$. Proof that line $AK$ bisects $\overline{XY}$.
AlphaGeometry formalization: a b c = triangle; i = incenter a b c; j = excenter a b c; o = circumcenter a b c; m1 = midpoint a i; x = on_circle o a, on_circle m1 a; m2 = midpoint a j; y = on_circle o a, on_circle m2 a; k = on_line b c, on_bline i j; m = midpoint x y ? coll a k m
HAGeo formalization: A B C = acute_triangle; I = incenter A B C; J = excenter A B C; O = circumcenter A B C; (ABC) = circle_center_point O A; M1 = midpoint A I; (M1) = circle_center_point M1 A; X = intersection (ABC) (M1); M2 = midpoint A J; (M2) = circle_center_point M2 A; Y = intersection (ABC) (M2); BC = line B C; l1 = perpendicular_bisector I J; K = intersection BC l1; M = midpoint X Y; Prove: collinear A K M
Difficulty score: 3.2