Problem (2016IranGOMp4): Let $\omega$ be the circumcircle of right-angled triangle $ABC$ ($\angle A = 90^{\circ}$). The tangent to $\omega$ at point $A$ intersects the line $BC$ at point $P$. Suppose that $M$ is the midpoint of the minor arc $AB$, and $PM$ intersects $\omega$ for the second time in $Q$. The tangent to $\omega$ at point $Q$ intersects $AC$ at $K$. Prove that $\angle PKC = 90^{\circ}$.
AlphaGeometry formalization: a b c = r_triangle; o = circumcenter a b c; p = on_line b c, on_tline a o a; m = on_circle o a, on_bline a b; q = on_line p m, on_circle o a; k = on_line a c, on_tline q o q ? perp p k a c
HAGeo formalization: A B C = right_triangle; O = circumcenter A B C; (O) = circle_center_point O A; l1 = tangent_line A (O); BC = line B C; P = intersection l1 BC; M = midarc_no A B C; MP = line M P; Q = intersection MP (O); l2 = tangent_line Q (O); AC = line A C; K = intersection l2 AC; KP = line K P; CK = line C K; Prove: perpendicular KP CK
Difficulty score: 2.3