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:

\begin{equation} x_1 - \alpha \nu_1 = 0 \label{eq:1} \end{equation}
\begin{equation} y_1 - 1 - \alpha\nu_2 = 0 \label{eq:2} \end{equation}
\begin{equation*} (x_1-a)^2 + y_1^2 = 1+a^2 \end{equation*}

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

\begin{equation*} (\nu_1^2 + \nu_2^2) \alpha^2 + 2(\nu_2 - \nu_1)\alpha = 0 \end{equation*}

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

\begin{equation} (\nu_1^2 + \nu_2^2)\alpha + 2(\nu_2 - \nu_1) = 0 \label{eq:3} \end{equation}

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:

\begin{align*} h_1 &= g_1 & h_5 &= g_7 & h_9 &= g_3 \\ h_2 &= g_2 & h_6 &= g_8 & h_{10} &= g_6 \\ h_3 &= g_3 & h_7 &= g_{10} & h_{11} &= g_9 \\ h_4 &= g_5 & h_8 &= g_{11} & h_{12} &= g_{12} \end{align*}

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

\begin{equation*} \nu_1^2 + \nu_2^2 \neq 0\qquad \omega_1^2+\omega_2^2 \neq 0 \end{equation*}