Problem (2016ARMOg10p2): Diagonals $AC,BD$ of cyclic quadrilateral $ABCD$ intersect at $P$.Point $Q$ is on$BC$ (between$B$ and $C$) such that $PQ \perp AC$.Prove that the line passes through the circumcenters of triangles $APD$ and $BQD$ is parallel to $AD$.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; p = on_line a c, on_line b d; q = on_line b c, on_tline p a c; o1 = circumcenter a p d; o2 = circumcenter b q d ? para o1 o2 a d
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; D = on_circle (ABC); AC = line A C; BD = line B D; P = intersection AC BD; l1 = perpendicular_line P AC; BC = line B C; Q = intersection BC l1; Oa = circumcenter A P D; Ob = circumcenter B Q D; OaOb = line Oa Ob; AD = line A D; Prove: parallel OaOb AD
Difficulty score: 2.3