ALC Seminar | Speaker: Herman Geuvers (Radboud University Nijmegen, The Netherlands)
Title: Computer Assisted Mathematical Proofs: using the computer to verify proofs
Abstract: A "Proof Assistant" is a computer program that allows users to create complete mathematical proofs, interactively with the computer, where the computer checks each small reasoning step. In this way one obtains the utmost guarantee of correctness.
We will outline the history of Proof Assistants and how they work, how they are used to verify mathematical proofs and computer systems (software and hardware). Verifying a proof with a PA is a lot of work, but as mathematical proofs get more and more difficult and complex there is an increasing use of PAs for mathematical proofs. Also for critical computer components it will pay off to verify them completely using a PA.
We will discuss why one would trust a PA and their limitations in use, which basically rest on the limitations of proof automation. It has recently become clear that methods from AI, especially Machine Learning and Large Language Models, apply very well to speeding up proof automation, and has brought some large developments.