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

• URL: http://arxiv.org/abs/2511.14728v1
• Date: Tue, 18 Nov 2025 18:20:17 GMT
• Title: Automated proving in planar geometry based on the complex number identity method and elimination
• Abstract summary: We improve the complex number identity proving method to a fully automated procedure, based on elimination ideals.<n>Our results are presented in Mathematica, Maple and in a new version of the Giac computer algebra system.
• Score: 0.9668407688201359
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• Real-rootedness of the Poincaré polynomials of $\overline{\mathcal M}_{0,n}$: an AI-assisted proof [0.0]
  We prove real-rootedness of the Poincaré [ P_n(t)=sum_i=0n-3 dim H2i(overlinemathcal M_0,n;mathbbQ) of the Deligne-Mumford moduli space.
  arXiv  Detail & Related papers  (2026-05-27T22:26:05Z)
• Information-Computation Tradeoffs for Noiseless Linear Regression with Oblivious Contamination [65.37519531362157]
  We show that any efficient Statistical Query algorithm for this task requires VSTAT complexity at least $tildeOmega(d1/2/alpha2)$.
  arXiv  Detail & Related papers  (2025-10-12T15:42:44Z)
• Accelerated Evolving Set Processes for Local PageRank Computation [75.54334100808022]
  This work proposes a novel framework based on nested evolving set processes to accelerate Personalized PageRank computation.<n>We show that the time complexity of such localized methods is upper bounded by $mintildemathcalO(R2/epsilon2), tildemathcalO(m)$ to obtain an $epsilon$-approximation of the PPR vector.
  arXiv  Detail & Related papers  (2025-10-09T09:47:40Z)
• A New Quantum Linear System Algorithm Beyond the Condition Number and Its Application to Solving Multivariate Polynomial Systems [7.587280395664776]
  A quantum linear system (QLS) problem asks for the preparation of a quantum state $|vecyrangle$ proportional to the solution of $Avecy = vecb$.<n>We present a new QLS algorithm that explicitly leverages the structure of the right-hand side vector $vecb$.
  arXiv  Detail & Related papers  (2025-10-07T05:28:25Z)
• A computational transition for detecting multivariate shuffled linear regression by low-degree polynomials [0.0]
  We investigate the model $Y=tfrac1sqrt1+sigma2(Pi_* X Q_* + sigma Z)<n>Consider the hypothesis testing problem of distinguishing this model from the case where $X$ and $Y$.<n>Results establish a smooth transition in the effectiveness of low-degree algorithms for this problem.
  arXiv  Detail & Related papers  (2025-04-04T00:32:38Z)
• Learning and Computation of $Φ$-Equilibria at the Frontier of Tractability [85.07238533644636]
  $Phi$-equilibria is a powerful and flexible framework at the heart of online learning and game theory.<n>We show that an efficient online algorithm incurs average $Phi$-regret at most $epsilon$ using $textpoly(d, k)/epsilon2$ rounds.<n>We also show nearly matching lower bounds in the online setting, thereby obtaining for the first time a family of deviations that captures the learnability of $Phi$-regret.
  arXiv  Detail & Related papers  (2025-02-25T19:08:26Z)
• Efficient Solution of Point-Line Absolute Pose [52.775981113238046]
  We revisit certain problems of pose estimation based on 3D--2D correspondences between features which may be points or lines. We show experimentally that the resulting solvers are numerically stable and fast.
  arXiv  Detail & Related papers  (2024-04-25T12:09:16Z)
• Solving Dense Linear Systems Faster Than via Preconditioning [1.8854491183340518]
  We show that our algorithm has an $tilde O(n2)$ when $k=O(n0.729)$. In particular, our algorithm has an $tilde O(n2)$ when $k=O(n0.729)$. Our main algorithm can be viewed as a randomized block coordinate descent method.
  arXiv  Detail & Related papers  (2023-12-14T12:53:34Z)
• Learning Hierarchical Polynomials with Three-Layer Neural Networks [56.71223169861528]
  We study the problem of learning hierarchical functions over the standard Gaussian distribution with three-layer neural networks. For a large subclass of degree $k$s $p$, a three-layer neural network trained via layerwise gradientp descent on the square loss learns the target $h$ up to vanishing test error. This work demonstrates the ability of three-layer neural networks to learn complex features and as a result, learn a broad class of hierarchical functions.
  arXiv  Detail & Related papers  (2023-11-23T02:19:32Z)
• Yuille-Poggio's Flow and Global Minimizer of Polynomials through Convexification by Heat Evolution [5.976447444084449]
  This study examines the convexification version of the backward differential flow algorithm for the global minimization ofs, introduced by O. Arikan textitet al in citeABK. We employ the heat evolution method for convexification combined with filtering, which acts as a cumulative form of Steklov's regularization. For quartics, our analysis not only reflects the results of O. Arikan et al. citeABK but also presents a significantly simpler version of Newton's method that can always globally minimize quartics without convexification.
  arXiv  Detail & Related papers  (2023-01-01T02:08:32Z)
• Mutually unbiased bases: polynomial optimization and symmetry [1.024113475677323]
  A set of $k$ orthonormal bases of $mathbb Cd$ is called mutually unbiased $|langle e,frangle |2 = 1/d$ whenever $e$ and $f$ are basis vectors in distinct bases. We exploit this symmetry (analytically) to reduce the size of the semidefinite programs making them tractable.
  arXiv  Detail & Related papers  (2021-11-10T14:14:53Z)
• Nonparametric Learning of Two-Layer ReLU Residual Units [22.870658194212744]
  We describe an algorithm that learns two-layer residual units with rectified linear unit (ReLU) activation. We design layer-wise objectives as functionals whose analytic minimizers express the exact ground-truth network in terms of its parameters and nonlinearities. We prove the statistical strong consistency of our algorithm, and demonstrate the robustness and sample efficiency of our algorithm by experiments.
  arXiv  Detail & Related papers  (2020-08-17T22:11:26Z)
• Model-Free Reinforcement Learning: from Clipped Pseudo-Regret to Sample Complexity [59.34067736545355]
  Given an MDP with $S$ states, $A$ actions, the discount factor $gamma in (0,1)$, and an approximation threshold $epsilon > 0$, we provide a model-free algorithm to learn an $epsilon$-optimal policy. For small enough $epsilon$, we show an improved algorithm with sample complexity.
  arXiv  Detail & Related papers  (2020-06-06T13:34:41Z)
• Learning sums of powers of low-degree polynomials in the non-degenerate case [2.6109033135086777]
  We give a learning algorithm for an arithmetic circuit model from a lower bound for the same model, provided certain non-degeneracy conditions hold. Our algorithm is based on a scheme for obtaining a learning algorithm for an arithmetic circuit model from a lower bound for the same model.
  arXiv  Detail & Related papers  (2020-04-15T06:18:41Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.