The eyeball theorem states that given two circles, the tangents from the center of each circle
to the sides of the other determine two line segments 
and 
of equal length.
The theorem can be proved by brute force by setting up the nine equations
 |  |  |
(1)
|
 |  |  |
(2)
|
 |  |  |
(3)
|
 |  |  |
(4)
|
 |  |  |
(5)
|
 |  |  |
(6)
|
 |  |  |
(7)
|
 |  |  |
(8)
|
 |  |  |
(9)
|
and using Gröbner basis to determine the polynomial equations satisfied by 
and 
while eliminate 
,
, 
, 
, 
, 
, and 
. The resulting eighth-degree polynomials satisfied by 
and 
are identical, proving that 
.
