Problem (2003CHNGaoLian): From point $P$ outside a circle draw two tangents to the circle touching at $A$ and $B$. Draw a secant line intersecting the circle at points $C$ and $D$, with $C$ between $P$ and $D$. Choose point $Q$ on the chord $CD$ such that $\angle DAQ=\angle PBC$. Prove that $\angle DBQ=\angle PAC$.
AlphaGeometry formalization: o = free; a0 = free; p = free; a b = tangent a b p o a0; c = on_circle o a0; d = on_line p c, on_circle o a0; q = on_line c d, on_aline q a d c b p ? eqangle d b b q p a a c
HAGeo formalization: (O) = circle; P = outside (O); l1 l2 = tangent P (O); A = intersection l1 (O); B = intersection l2 (O); C = on_circle (O); CP = line C P; D = intersection CP (O); CD = line C D; l3 = angle_equal1 A D C B P; Q = intersection CD l3; Prove: equal_angle D B Q P A C
Difficulty score: 1.5