Problem (2021CGMOp7): In an acute triangle $ABC$, $AB \neq AC$, $O$ is its circumcenter. $K$ is the reflection of $B$ over $AC$ and $L$ is the reflection of $C$ over $AB$. $X$ is a point within $ABC$ such that $AX \perp BC, XK=XL$. Points $Y, Z$ are on $\overline{BK}, \overline{CL}$ respectively, satisfying $XY \perp CK, XZ \perp BL$. Proof that $B, C, Y, O, Z$ lie on a circle.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; k = reflect b a c; l = reflect c a b; x = on_tline a b c, on_bline k l; y = on_line b k, on_tline x c k; z = on_line c l, on_tline x b l ? cyclic b c y o
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; AC = line A C; K = reflect_point_wrt_line B AC; AB = line A B; L = reflect_point_wrt_line C AB; BC = line B C; l1 = perpendicular_line A BC; l2 = perpendicular_bisector K L; X = intersection l1 l2; CK = line C K; l3 = perpendicular_line X CK; BK = line B K; Y = intersection BK l3; BL = line B L; l4 = perpendicular_line X BL; CL = line C L; Z = intersection CL l4; Prove: concyclic B C Y O
Difficulty score: 3.7