Problem (2012G4): Let $ABC$ be a triangle with $AB \neq AC$ and circumcenter $O$. The bisector of $\angle BAC$ intersects $BC$ at $D$. Let $E$ be the reflection of $D$ with respect to the midpoint of $BC$. The lines through $D$ and $E$ perpendicular to $BC$ intersect the lines $AO$ and $AD$ at $X$ and $Y$ respectively. Prove that the quadrilateral $BXCY$ is cyclic.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_line b c, angle_bisector b a c; m = midpoint b c; e = mirror d m; x = on_line a o, on_tline d b c; y = on_line a d, on_tline e b c ? cyclic b x c 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; M = midpoint B C; E = reflect D M; l2 = perpendicular_line D BC; AO = line A O; X = intersection l2 AO; l3 = perpendicular_line E BC; AD = line A D; Y = intersection l3 AD; Prove: concyclic B X C Y
Difficulty score: 2.5