Proving Geometric Theorems about Ruler-and-Compass Constructions

 

After my M.S. in Mathematics I worked on Automatic Theorem Proving in Geometry and more precisely on randomized methods for proving Geometric theorems in the classical rule-and-compass setting. The main goal of this project was to reduce the computational complexity of previous methods (i.e., Wu's method is exponential and methods based on Groebner bases that are doubly exponential), and propose a method that could be applied also to Real Geometry. Our  key idea consists of proving the validity of a conjecture by examples, randomly generating instances of its construction. We first investigated randomized version of Wu's prover using the Schwartz randomized zero-test for multivariate polynomials but without success because of the huge cardinality of its test set. Indeed, experiments conducted on a prototype showed that Wu's method was faster than its probabilistic version. These results motivated us to explore a different probabilistic approach that combines symbolic and numerical computations and that addresses conjectures constructed by rule-and-compass. The key idea of our method is to transform the problem of verifying a geometric conjecture into the problem of verifying the vanishing of a radical expression. This conducted us to study another problem of independent interest: the generalization of the Schwartz zero-test to radical expressions (including divisions and square roots operators).  Our probabilistic method, which is based on a novel randomized zero-test for radical expressions, is the first practical method with polynomial time complexity, and generalizes Wu's method for proving theorems in Real Geometry. Experiments run on our system show the practicality of this method and its better performance in many cases over Wu’s method. For instance, it can be employed efficiently to quickly reject false geometric conjectures.
I completed this project at NYU with the collaboration of Professor Chee Yap and Chen Li, who contributed particularly to issues related to the exact geometric computation. The prover system is part of the Core library and it is currently downloadable as its application.



D. Tulone, C. K. Yap, and C. Li. Randomized zero-testing of radical expressions and Elementary Geometry theorem proving. In Automated Deduction in Geometry, LNCS 2061, pp. 58-82, Springer 2001.