# 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:

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

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

Let \( g_1(x_1,\alpha) \), \( g_2(y_1,\alpha) \) and \( g_3(\alpha) \) be polynomials obtained from \( \eqref{eq:1}, \eqref{eq:2}, \eqref{eq: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:

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