Problem (2012EGMOp1): Let $ABC$ be a triangle with circumcentre $O$. The points $D,E,F$ lie in the interiors of the sides $BC,CA,AB$ respectively, such that $DE$ is perpendicular to $CO$ and $DF$ is perpendicular to $BO$. (By interior we mean, for example, that the point $D$ lies on the line $BC$ and $D$ is between $B$ and $C$ on that line.) Let $K$ be the circumcentre of triangle $AFE$. Prove that the lines $DK$ and $BC$ are perpendicular.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = on_line b c; e = on_line a c, on_tline d c o; f = on_line a b, on_tline d b o; k = circumcenter a e f ? perp d k b c
HAGeo formalization: A B C = triangle; O = circumcenter A B C; BC = line B C; D = foot O BC; CO = line C O; E = foot D CO; BO = line B O; F = foot D BO; K = circumcenter A F E; DK = line D K; Prove: perpendicular DK BC
Difficulty score: 1.3