Problem (2024KoMaLA877): A convex quadrilateral $ABCD$ is circumscribed about circle $\omega$. A tangent to $\omega$ parallel to $AC$ intersects $BD$ at a point $P$ outside of $\omega$. The second tangent from $P$ to $\omega$ touches $\omega$ at a point $T$. Prove that $\omega$ and circumcircle of $ATC$ are tangent.
AlphaGeometry formalization: t1 t2 t3 = triangle; i = circumcenter t1 t2 t3; t4 = on_circle i t1; a = on_tline t1 i t1, on_tline t2 i t2; b = on_tline t2 i t2, on_tline t3 i t3; c = on_tline t3 i t3, on_tline t4 i t4; d = on_tline t1 i t1, on_tline t4 i t4; t5 = on_circle i t1, on_tline i a c; p = on_tline t5 i t5, on_line b d; t = reflect t5 i p; o = circumcenter a t c ? coll i o t
HAGeo formalization: T1 T2 T3 = triangle; I = circumcenter T1 T2 T3; (I) = circle_center_point I T1; T4 = on_circle (I); IT1 = line I T1; IT2 = line I T2; IT3 = line I T3; IT4 = line I T4; l1 = perpendicular_line T1 IT1; l2 = perpendicular_line T2 IT2; A = intersection l1 l2; l3 = perpendicular_line T3 IT3; B = intersection l2 l3; l4 = perpendicular_line T4 IT4; C = intersection l3 l4; D = intersection l1 l4; AC = line A C; l5 = perpendicular_line I AC; T5 = intersection (I) l5; IT5 = line I T5; l6 = perpendicular_line T5 IT5; BD = line B D; P = intersection l6 BD; IP = line I P; T = reflect_point_wrt_line T5 IP; O = circumcenter A T C; Prove: collinear I O T
Difficulty score: 4.9