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.