Limits of Theorem Proving

The notions of proofs and theorems are central to mathematics. We aim to explore the mathematical limits of theorem proving. To formalize the limits of the human process of elaborating proofs, we consider computational resources and we focus on the following questions: What is the tradeoff between the computational strength of the resources and the efficiency in proving theorems? Does theorem proving become easier when proofs are verified with more powerful resources? Can theorem proving be automated? Approaching such questions using powerful models as quantum or randomized computations is at a very early stage of investigation. But quantum and randomized computational resources are deeply investigated in the theory that studies the efficiency requirements of computational problems. We plan to apply the techniques of this fruitful research to our questions. Closely collaborating with leading experts in the field we plan to explore the limitations of theorem proving with respect to these new computational models. The main output of the project will be theoretical investigation in form of high quality research papers. The project continues an eight months collaboration between Nicola Galesi and Olaf Beyersdorff from October 2009 to May 2010 and will amplify the interaction between the two groups in Rome and Hanover. We plan to discuss our new approach with a broader audience of computer scientists, mathematicians, physicists, and philosophers organizing a workshop in the Bertinoro Residential Center for Informatics in Italy. We expect that due to the results from our project and due to dissemination of these results at the workshop, also other research groups will get interested in exploring theorem proving with non-classical models of computation. As enduring impact, we consider our project a starting point for the creation of a well-connected network and community of researchers interested and investigating in the field of mathematical limits of theorem proving.