Problem (2019USEMOp6): Let $ABC$ be an acute scalene triangle with circumcenter $O$ and altitudes $\overline{AD}$, $\overline{BE}$, $\overline{CF}$. Let $X$, $Y$, $Z$ be the midpoints of $\overline{AD}$, $\overline{BE}$, $\overline{CF}$. Lines $AD$ and $YZ$ intersect at $P$, lines $BE$ and $ZX$ intersect at $Q$, and lines $CF$ and $XY$ intersect at $R$. Suppose that lines $YZ$ and $BC$ intersect at $A'$, and lines $QR$ and $EF$ intersect at $D'$. Prove that the perpendiculars from $A$, $B$, $C$, $O$, to the lines $QR$, $RP$, $PQ$, $A'D'$, respectively, are concurrent.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; d = foot a b c; e = foot b a c; f = foot c a b; x = midpoint a d; y = midpoint b e; z = midpoint c f; p = on_line a d, on_line y z; q = on_line b e, on_line z x; r = on_line c f, on_line x y; a1 = on_line y z, on_line b c; d1 = on_line q r, on_line e f; k1 = on_tline a q r, on_tline b r p ? perp k1 o a1 d1
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; BC = line B C; D = foot A BC; AC = line A C; E = foot B AC; AB = line A B; F = foot C AB; X = midpoint A D; Y = midpoint B E; Z = midpoint C F; AD = line A D; YZ = line Y Z; P = intersection AD YZ; BE = line B E; XZ = line X Z; Q = intersection BE XZ; CF = line C F; XY = line X Y; R = intersection CF XY; A1 = intersection YZ BC; QR = line Q R; EF = line E F; D1 = intersection QR EF; l1 = perpendicular_line A QR; PR = line P R; l2 = perpendicular_line B PR; A1D1 = line A1 D1; K1 = intersection l1 l2; K1O = line K1 O; Prove: perpendicular K1O A1D1
Difficulty score: 4.8