Problem (2011BalkanMOp1): Let $ABCD$ be a cyclic quadrilateral which is not a trapezoid and whose diagonals meet at $E$. The midpoints of $AB$ and $CD$ are $F$ and $G$ respectively, and $\ell$ is the line through $G$ parallel to $AB$. The feet of the perpendiculars from E onto the lines $\ell$ and $CD$ are $H$ and $K$, respectively. Prove that the lines $EF$ and $HK$ are perpendicular.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; e = on_line a c, on_line b d; f = midpoint a b; g = midpoint c d; s = on_pline g a b; h = foot e g s; k = foot e c d ? perp e f h k
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); AC = line A C; BD = line B D; E = intersection AC BD; F = midpoint A B; G = midpoint C D; AB = line A B; l = parallel_line G AB; H = foot E l; CD = line C D; K = foot E CD; EF = line E F; HK = line H K; Prove: perpendicular EF HK
Difficulty score: 1.7