Problem (2024ARMOg10p6): Let $ABCD$ be a parallelogram. Let $M$ be the midpoint of the arc $AC$ containing $B$ of the circumcircle of $ABC$ . Let $E$ be a point on segment $AD$ and $F$ a point on segment $CD$ such that $ME=MD=MF$. Show that $BMEF$ is cyclic.
AlphaGeometry formalization: a b c = triangle; d = parallelogram a b c d; o = circumcenter a b c; m = on_circle o a, on_bline a c; e = on_line a d, on_circle m d; f = on_line c d, on_circle m d ? cyclic b m e f
HAGeo formalization: A B C D = parallelogram; O = circumcenter A B C; M = midarc A B C; AD = line A D; (M,D) = circle_center_point M D; E = intersection AD (M,D); CD = line C D; F = intersection CD (M,D); Prove: concyclic B M E F
Difficulty score: 3.5