After my MS in Mathematics I started exploring Automatic Theorem Proving in Geometry, and more precisely randomized methods for proving geometric conjecture in Elementary Geometry. The main target was to improve their complexity since all previous methods showed high complexity. Among the well—known methods to prove theorems in Elementary Geometry using constructive methods, the most popular are the followings:
Methods based on Groebner bases are general but their worst case time complexity is double-exponential. The complexity of Wu method is only single-exponential, however it proves theorems in Geometry based on algebraically closed fields, such as Complex Geometry, but not in Real Geometry. This drawback is overcome by methods based on cell decomposition which address Real Geometry and are general, though they remain slow in practice.
The underlying idea of my research was to prove the validity of a conjecture by examples, similarly to Hong’s proposal. That is, to test the validity of conjectures on randomly generating instances of its construction. A randomized version of Wu's prover, using Schwartz zero-test for multivariate polynomials was explored but without success because of the very large constants defining the test set. In fact, experiments conducted on a prototype of this method and on Wu’s method showed a better performance of Wu’s method over the previous one. These results motivated me to explore a different probabilistic approach that combines symbolic computations and numerical computations and that addresses conjectures constructed by rule and compass. The basic idea is to transform the verification of a geometric conjecture into the problem of verifying the vanishing of a radical expression. This conducted me to another problem and result, of independent interest: the generalization of Schwartz zero-test to radical expressions (including divisions and square roots operators).
Our probabilistic approach, based on a novel randomized zero-test for radical expressions, is the first method with polynomial time complexity, and generalizes Wu's method for proving theorems in Real Geometry. Experiments run on our probabilistic prover show the practicality of this method and its better performance in many cases over Wu’s method. case of false It can be employed efficiently to quickly reject false geometric conjectures.
Chee Yap and Chen Li contributed to the last phase of this project, in particular for the issues related to the exact computations. The prover is part of the Core library and it is currently downloadable as its main application.
For details, D.Tulone, C.Yap, C.Li Randomized Zero Testing of Radical Expressions and Elementary Geometry Theorem Proving, in Proc. Int'l Workshop on Automated Deduction in Geometry (ADG'00). The full version can also be found in LNCS/LNAI 2061.