Problem (2006CTSTp7): The centre of the circumcircle of quadrilateral $ABCD$ is $O$ and $O$ is not on any of the sides of $ABCD$. $P=AC \cap BD$. The circumecentres of $\triangle{OAB}$, $\triangle{OBC}$, $\triangle{OCD}$ and $\triangle{ODA}$ are $O_1$, $O_2$, $O_3$ and $O_4$ respectively. Prove that $O_1O_3$, $O_2O_4$ and $OP$ are concurrent.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; o = circumcenter a b c; p = on_line a c, on_line b d; o1 = circumcenter o a b; o2 = circumcenter o b c; o3 = circumcenter o c d; o4 = circumcenter o d a; x = on_line o1 o3, on_line o2 o4 ? coll o p x
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); O = circumcenter A B C; AC = line A C; BD = line B D; P = intersection AC BD; O1 = circumcenter O A B; O2 = circumcenter O B C; O3 = circumcenter O C D; O4 = circumcenter O D A; O1O3 = line O1 O3; O2O4 = line O2 O4; X = intersection O1O3 O2O4; Prove: collinear O P X
Difficulty score: 3.0