Problem (2012CHNWesternMOp5): $O$ is the circumcenter of acute $\Delta ABC$, $H$ is the Orthocenter. $AD \bot BC$, $EF$ is the perpendicular bisector of $AO$,$D,E$ on the $BC$. Prove that the circumcircle of $\Delta ADE$ through the midpoint of $OH$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; d = foot a b c; e = on_line b c, on_bline a o; n = midpoint o h ? cyclic a d e n
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; H = orthocenter A B C; BC = line B C; D = foot A BC; l1 = perpendicular_bisector A O; E = intersection l1 BC; N = midpoint O H; Prove: concyclic A D E N
Difficulty score: 2.0