Problem (2024PolandMOp6): Let $ABCD$ be a parallelogram. Let $X \notin AC $ lie inside $ABCD$ so that $\angle AXB = \angle CXD = 90^ {\circ}$ and $\Omega$ denote the circumcircle of $AXC$. Consider a diameter $EF$ of $\Omega$ and assume neither $E, \ X, \ B$ nor $F, \ X, \ D$ are collinear. Let $K \neq X$ be an intersection point of circumcircles of $BXE$ and $DXF$ and $L \neq X$ be such point on $\Omega$ so that $\angle KXL = 90^{\circ}$. Prove that $AB = KL$.
AlphaGeometry formalization: a b c = triangle; d = parallelogram a b c d; m_ab = midpoint a b; m_cd = midpoint c d; x = on_circle m_ab a, on_circle m_cd c; o = circumcenter a x c; e = on_circle o a; f = mirror e o; o1 = circumcenter b x e; o2 = circumcenter d x f; k = on_circle o1 b, on_circle o2 d; l = on_circle o a, on_tline x x k ? cong a b k l
HAGeo formalization: A B C = triangle; D = parallelogram A B C; M_ab = midpoint A B; M_cd = midpoint C D; (AB) = circle_center_point M_ab A; (CD) = circle_center_point M_cd C; X = intersection (AB) (CD); O = circumcenter A X C; (AXC) = circle_center_point O A; E = on_circle (AXC); F = reflect_point_wrt_point E O; O1 = circumcenter B X E; O2 = circumcenter D X F; (BXE) = circle_center_point O1 B; (DXF) = circle_center_point O2 D; K = intersection (BXE) (DXF); XK = line X K; l1 = perpendicular_line X XK; L = intersection (AXC) l1; Prove: cong A B K L
Difficulty score: 4.6