Problem (2005CHNSouthEastMOp2): Circle $C$ (with center $O$) does not have common point with line $l$. Draw $OP$ perpendicular to $l$, $P \in l$. Let $Q$ be a point on $l$ ($Q$ is different from $P$), $QA$ and $QB$ are tangent to circle $C$, and intersect the circle at $A$ and $B$ respectively. $AB$ intersects $OP$ at $K$. $PM$, $PN$ are perpendicular to $QB$, $QA$, respectively, $M \in QB$, $N \in QA$. Prove that segment $KP$ is bisected by line $MN$.
AlphaGeometry formalization: o = free; r1 = free; p = free; q = on_tline p o p; a b = tangent a b q o r1; k = on_line a b, on_line o p; m = foot p q b; n = foot p q a; x = midpoint k p ? coll x m n
HAGeo formalization: (O) = circle; O = circumcenter (O); l = line; P = foot O l; Q = on_line l; A B = tangent_point Q (O); OP = line O P; AB = line A B; K = intersection OP AB; BQ = line B Q; M = foot P BQ; AQ = line A Q; N = foot P AQ; X = midpoint K P; Prove: collinear X M N
Difficulty score: 2.6