Problem (2013RMMp3): Let $ABCD$ be a quadrilateral inscribed in a circle $\omega$. The lines $AB$ and $CD$ meet at $P$, the lines $AD$ and $BC$ meet at $Q$, and the diagonals $AC$ and $BD$ meet at $R$. Let $M$ be the midpoint of the segment $PQ$, and let $K$ be the common point of the segment $MR$ and the circle $\omega$. Prove that the circumcircle of the triangle $KPQ$ and $\omega$ are tangent to one another.
AlphaGeometry formalization: a b c = triangle; d = on_circum a b c; o = circumcenter a b c; p = on_line a b, on_line c d; q = on_line a d, on_line b c; r = on_line a c, on_line b d; m = midpoint p q; k = on_line m r, on_circle o a; o1 = circumcenter k p q ? coll o o1 k
HAGeo formalization: A B C = triangle; O = circumcenter A B C; (ABC) = circle_center_point O A; D = on_circle (ABC); AB = line A B; CD = line C D; P = intersection AB CD; AD = line A D; BC = line B C; Q = intersection AD BC; AC = line A C; BD = line B D; R = intersection AC BD; M = midpoint P Q; MR = line M R; K = intersection MR (ABC); O1 = circumcenter K P Q; Prove: collinear O O1 K
Difficulty score: 4.0