Home > Geometry > Mechanical Geometry Theorem Proving

## Mechanical Geometry Theorem Proving

In 1977, Professor Wen-Tsun Wu succeeded in developing a method of mechanical geometry theorem proving. This method has been applied to prove or even discover hundreds of non-trivial difficult theorems in elementary and differential geometries on a computer in an almost trivial manner. Usign Ritt’s differential algebra, Wu established a method for solving algebraic and differential equations by transforming an equation system in the general form to equation systems in triangular form. This is the Ritt-Wu decomposition algorithm, that later on was shown to be equivalent to perform a series of operations on ideals, very easily carried out by means of Gröbner basis manipulation.

I wrote a script in MAPLE to perform evaluations of the validity of some simple theorems in Euclidean Geometry, and wrote a small paper (in Spanish) on one of my findings, that was published in Bol. Asoc. Prof. Puig Adams, in October’99: “Sobre demostración automática de un problema geométrico“.

The example I cover in that short article can be seen below.

Given: Circles $A$, $B$ that intersect each other in points $C$ and $D$, and given points $E$, $F$ in circle $A$, consider line $a$ through $E$ and $C$, and line $b$ through $F$ and $D$. The intersections of line $a$ with circle $A$ are $C$ and $G$. The intersections of line $b$ with circle $B$ are $D$ and $H$. Consider the segments $c$ (connecting $E$ with $F$) and $d$ (connecting $G$ with $H$).

To prove: Segments $c$ and $d$ are parallel.

### Proposed Solution

Let us assume the points $C$ and $D$ have coordinates $C=(0,1)$ and $D=(0,-1)$, and the centers of the circles are $A=(a,0)$, $B=(b,0)$.  Let us consider a vector $\nu = (\nu_1, \nu_2)$ supported in the point $C$, and a vector $\omega = (\omega_1, \omega_2)$ supported in the point $D$.

A line through $C$ with leading vector $\nu$ intersects the circle $A$ at the point $E=(x_1,y_1)$. In order to compute its coordinates, we consider the equations of the line and the circle:

 (1) $x_1 - \alpha \nu_1 = 0$ (2) $y_1 - 1 - \alpha\nu_2 = 0$ $(x_1-a)^2 + y_1^2 = 1+a^2$

By simple substitution, we obtain the following second-degree equation, stating the condition:

$(\nu_1^2 + \nu_2^2) \alpha^2 + 2(\nu_2 - \nu_1)\alpha = 0$

One of the solutions is the trivial $\alpha=0$ (the point $C$). The other solution is what we need:

 (3) $(\nu_1^2 + \nu_2^2)\alpha + 2(\nu_2 - \nu_1) = 0$

Let $g_1(x_1,\alpha)$, $g_2(y_1,\alpha)$ and $g_3(\alpha)$ be polynomials obtained from (1), (2) and (3).  We obtain polynomials $g_4(x_2,\beta)$, $g_5(y_2, \beta)$ and $g_6(\beta)$ in a similar way, considering the condition of point $F$ belonging in the line through $D$ with leading vector $\omega$ and the circle $A$. We also obtain polynomials $g_7(x_3, \gamma)$, $g_8(y_3,\gamma)$ and $g_9(\gamma)$ for the point $G$ in circle $B$ and line through $C$ with leading vector $\nu$. Finally, obtain polynomials $g_{10}(x_4,\delta)$, $g_{11}(y_4,\delta)$ and $g_{12}(\delta)$ for point $H$ belonging to circle $B$ and the line through point $D$ with leading vector $\omega$.

We use the Ritt-Wu method on those polynomials (notice it is not necessary to turn the system in triangular, since by a simple re-ordering of the polynomials we accomplish this state).  The proof follows:

 $h_1 = g_1$ $h_2=g_2$ $h_3=g_3$ $h_4=g_5$ $h_5 = g_7$ $h_6=g_8$ $h_7 = g_{10}$ $h_8 = g_{11}$ $h_9 = g_3$ $h_{10} = g_6$ $h_{11}=g_9$ $h_{12} = g_{12}$

The degenerate conditions are then reduced to vectors $\nu$ and $\omega$ being not nill:

$\nu_1^2 + \nu_2^2 \neq 0\qquad \omega_1^2+\omega_2^2 \neq 0$