Problem (2014AsiaPacificMOp5): Circles $\omega$ and $\Omega$ meet at points $A$ and $B$. Let $M$ be the midpoint of the arc $AB$ of circle $\omega$ ($M$ lies inside $\Omega$). A chord $MP$ of circle $\omega$ intersects $\Omega$ at $Q$ ($Q$ lies inside $\omega$). Let $\ell_P$ be the tangent line to $\omega$ at $P$, and let $\ell_Q$ be the tangent line to $\Omega$ at $Q$. Prove that the circumcircle of the triangle formed by the lines $\ell_P$, $\ell_Q$ and $AB$ is tangent to $\Omega$.
AlphaGeometry formalization: a b = segment; o1 = on_bline a b; o2 = on_bline a b; m = on_circle o1 a, on_tline o1 a b; p = on_circle o1 a; q = on_line m p, on_circle o2 a; x = on_line a b, on_tline p o1 p; y = on_line a b, on_tline q o2 q; z = on_tline p o1 p, on_tline q o2 q; o3 = circumcenter x y z; t = on_circle o3 x, on_circle o2 a ? coll o2 o3 t
HAGeo formalization: A = point; B = point; l = perpendicular_bisector A B; O1 = on_line l; O2 = on_line l; (O1) = circle_center_point O1 A; (O2) = circle_center_point O2 A; M = intersection l (O1); P = on_circle (O1); MP = line M P; Q = intersection MP (O2); O1P = line O1 P; lp = perpendicular_line P O1P; O2Q = line O2 Q; lq = perpendicular_line Q O2Q; AB = line A B; X = intersection AB lp; Y = intersection AB lq; Z = intersection lp lq; O3 = circumcenter X Y Z; (XYZ) = circle_center_point O3 X; T = intersection (XYZ) (O2) Prove: collinear O2 O3 T
Difficulty score: 3.4