Problem (2021IranGOMp1): Let $ABC$ be a triangle with $AB = AC$. Let $H$ be the orthocenter of $ABC$. Point $E$ is the midpoint of $AC$ and point $D$ lies on the side $BC$ such that $3CD = BC$. Prove that $BE \perp HD$.
AlphaGeometry formalization: a b c = iso_triangle; h = orthocenter a b c; e = midpoint a c; d f = trisegment d f c b ? perp b e h d
HAGeo formalization: A B C = isos_triangle; H = orthocenter A B C; E = midpoint A C; D D1 = trisegment C B; BE = line B E; DH = line D H; Prove: perpendicular BE DH
Difficulty score: 1.6