眼球定理

給定兩個圓，從每個圓的圓心向另一個圓的邊作切線。那麼線段 和 的長度相等。

該定理可以透過暴力方法證明，即建立九個方程

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

並使用 Gröbner 基 來確定由 和 滿足的多項式方程，同時消除 , , , , , 和 。由 和 滿足的得到的八次多項式是相同的，證明了 。