[11-18] Computer Assisted Mathematical Proofs: Successes and Limitations
Title: Computer Assisted Mathematical Proofs: Successes and Limitations
Speaker: Herman Geuvers (Radboud University Nijmegen) http://www.cs.ru.nl/~herman/
Time: 9:30am, November 18th, 2016
Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, Chinese Academy of Sciences.
Mathematical proofs get more and more difficult and complex. At the same time more and more computer systems (software and hardware) can be verified rigidly using mathematical proof, so there is an increasing request for completely verified mathematical proofs.
The field of Computer Assisted Mathematical Proofs fills this gap by allowing users to create complete mathematical proofs, interactively with the computer, where the computer checks each small reasoning step.
In the talk, I will illustrate this with two examples where the computer has been used to completely verify a proof: (1) From pure mathematics: The proof of the Kepler conjecture (2) From computer science: The proof of the correctness of a C compiler.
Then I will discuss the present day limitations of Computer Assisted Mathematical Proofs, which basically rest on the limitations of proof automation.
It has recently become clear that Machine Learning provides methods that apply very well to speeding up proof automation. Machine Learning does not supersede standard techniques (from Automated Theorem Proving) but provide the ideal additional technique.
I will show how Machine Learning techniques fit in and what successes have been obtained in proof automation.