Problem (2011ARMOg9p2): Given is an acute angled triangle $ABC$. A circle going through $B$ and the triangle's circumcenter, $O$, intersects $BC$ and $BA$ at points $P$ and $Q$ respectively. Prove that the intersection of the heights of the triangle $POQ$ lies on line $AC$.
AlphaGeometry formalization: a b c = triangle; o = circumcenter a b c; k = on_bline b o; p = on_line b c, on_circle k b; q = on_line b a, on_circle k b; t = orthocenter p o q ? coll a c t
HAGeo formalization: A B C = acute_triangle; O = circumcenter A B C; l = perpendicular_bisector O B; K = on_line l; (K) = circle_center_point K O; BC = line B C; P = intersection (K) BC; AB = line A B; Q = intersection (K) AB; H = orthocenter P O Q; Prove: collinear H A C
Difficulty score: 2.3