Problem (2017G3): Let $O$ be the circumcenter of an acute triangle $ABC$. Line $OA$ intersects the altitudes of $ABC$ through $B$ and $C$ at $P$ and $Q$, respectively. The altitudes meet at $H$. Prove that the circumcenter of triangle $PQH$ lies on a median of triangle $ABC$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; h = orthocenter a b c; p = on_line o a, on_line b h; q = on_line o a, on_line c h; k = circumcenter p q h; m = midpoint b c ? coll k a m
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; H = orthocenter A B C; M = midpoint B C; AO = line A O; BH = line B H; P = intersection AO BH; CH = line C H; Q = intersection AO CH; O1 = circumcenter P Q H; Prove: collinear O1 A M
Difficulty score: 2.7