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

arXiv: https://arxiv.org/abs/2511.14728 · HTML: https://mlsanity.com/paper/2511.14728/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- First posted on arXiv 18 Nov 2025.

## Abstract (arXiv)

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 hi to hi-ri, 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 mathbbQ[r,r1,r2,ldots] we can find a conclusive result. It plays an important role that if r1,r2,ldots are real, r must also be real if there is a linear polynomial p(r)∈ 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.