眼球定理

给定两个圆，从每个圆的圆心向另一个圆的边作切线。那么线段 和 的长度相等。

该定理可以通过暴力方法证明，即建立九个方程

			(1)
			(2)
			(3)
			(4)
			(5)
			(6)
			(7)
			(8)
			(9)

并使用 Gröbner 基 来确定由 和 满足的多项式方程，同时消除 , , , , , 和 。由 和 满足的得到的八次多项式是相同的，证明了 。