Problem (2020AQGOp4): Line $\ell$ intersects sides $\overline{AB},\overline{AC}$ of $\triangle ABC$ at $D,E$. $P,Q$ are the midpoints of $\overline{CD}$ and $\overline{BE}$ respectively. The lines through $P,Q$ perpendicular to $\ell$ meet the perpendicular bisectors of $\overline{AC}$ and $\overline{AB}$ at $M,N$ respectively. Prove that $\overline{MN} \parallel \overline{PQ}$.
AlphaGeometry formalization: a b c = triangle; d = on_line a b; e = on_line a c; p = midpoint c d; q = midpoint b e; m = on_bline a c, on_tline p d e; n = on_bline a b, on_tline q d e ? para m n p q
HAGeo formalization: A B C = triangle; AB = line A B; D = on_line AB; AC = line A C; E = on_line AC; P = midpoint C D; Q = midpoint B E; DE = line D E; l1 = perpendicular_line P DE; l2 = perpendicular_line Q DE; m1 = perpendicular_bisector A C; M = intersection l1 m1; m2 = perpendicular_bisector A B; N = intersection l2 m2; MN = line M N; PQ = line P Q; Prove: parallel MN PQ
Difficulty score: 2.8