Problem (2006USATSTp6): Let $ABC$ be a triangle. Triangles $PAB$ and $QAC$ are constructed outside of triangle $ABC$ such that $AP = AB$ and $AQ = AC$ and $\angle{BAP}= \angle{CAQ}$. Segments $BQ$ and $CP$ meet at $R$. Let $O$ be the circumcenter of triangle $BCR$. Prove that $AO \perp PQ.$
AlphaGeometry formalization: a b c = triangle; p = on_circle a b; q = on_circle a c, on_aline q a c b a p; r = on_line b q, on_line c p; o = circumcenter b c r ? perp a o p q
HAGeo formalization: A B C = triangle; (A,B) = circle_center_point A B; P = on_circle (A,B); (A,C) = circle_center_point A C; l1 = angle_equal1 A C B A P; Q = intersection (A,C) l1; BQ = line B Q; CP = line C P; R = intersection BQ CP; O = circumcenter B C R; AO = line A O; PQ = line P Q; Prove: perpendicular AO PQ
Difficulty score: 3.2