Problem (2022CzechAPSlovakp5): Let $ABC$ be a triangle with $AB < AC$ and circumcenter $O$. The angle bisector of $\angle BAC$ meets the side $BC$ at $D$. The line through $D$ perpendicular to $BC$ meets the segment $AO$ at $X$. Furthermore, let $Y$ be the midpoint of segment $AD$. Prove that points $B, C, X, Y$ are concyclic.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_line b c, angle_bisector b a c; x = on_line a o, on_tline d b c; y = midpoint a d ? cyclic b c x y
HAGeo formalization: A B C = triangle; O = circumcenter A B C; l1 = angle_bisector B A C; BC = line B C; D = intersection l1 BC; l2 = perpendicular_line D BC; AO = line A O; X = intersection l2 AO; Y = midpoint A D; Prove: concyclic B C X Y
Difficulty score: 2.4