{"ID":2840179,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2511.14728","arxiv_id":"2511.14728","title":"Automated proving in planar geometry based on the complex number identity method and elimination","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.","short_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 varia...","url_abs":"https://arxiv.org/abs/2511.14728","url_pdf":"https://arxiv.org/pdf/2511.14728v1","authors":"[\"Zoltán Kovács\",\"Xicheng Peng\"]","published":"2025-11-18T18:20:17Z","proceeding":"cs.CG","tasks":"[\"cs.CG\",\"cs.AI\"]","methods":"[]","has_code":false}