Automated proving in planar geometry based on the complex number identity method and elimination

TL;DR

The paper presents a fully automated procedure for proving planar geometry statements by extending the complex-number identity method with elimination ideals. It rewrites hypotheses and the thesis with auxiliary variables, clears denominators via a Rabinowitsch trick, and extracts an elimination ideal $I$ in $ obreak\mathbb{Q}[r,r_1,r_2,\ldots]$ to derive conclusive results, including realness qualifications when linear polynomials appear in $I$. Implementations across Giac, Mathematica, and Maple, plus a GeoGebra Discovery prototype, demonstrate practical automatic proofs on classic theorems such as the converse of Thales’ circle theorem, Varignon’s parallelogram, and concurrent angle bisectors, with readable proof outputs. The work highlights both the potential and the limitations of elimination-based reasoning in dynamic geometry, pointing to future improvements in speed, degenerate cases, and higher-dimensional extensions.

Abstract

We improve the complex number identity proving method to a fully automated procedure, based on elimination ideals. By using declarative equations or rewriting each real-relational hypothesis $h_i$ to $h_i-r_i$, and the thesis $t$ to $t-r$, clearing the denominators and introducing an extra expression with a slack variable, we eliminate all free and relational point variables. From the obtained ideal $I$ in $\mathbb{Q}[r,r_1,r_2,\ldots]$ we can find a conclusive result. It plays an important role that if $r_1,r_2,\ldots$ are real, $r$ must also be real if there is a linear polynomial $p(r)\in I$, unless division by zero occurs when expressing $r$. Our results are presented in Mathematica, Maple and in a new version of the Giac computer algebra system. Finally, we present a prototype of the automated procedure in an experimental version of the dynamic geometry software GeoGebra.

Figures (4)

• Figure 1: Examples 1 and 2: The converse of Thales' Circle Theorem
• Figure 2: Example 3: Medians of a triangle are concurrent
• Figure 3: Example 4: The midpoint parallelogram in GeoGebra Discovery
• Figure 4: Example 4: Angle bisectors of a triangle are concurrent, constructed in GeoGebra Discovery