Seminar Announcement

　　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.

　　Abstract:

　　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.