Fabian Lukas Grubmüller: Demystifying Proof Assistants: An Introduction to Interactive Theorem Proving

Abstract

 Interactive theorem proving (ITP) is a powerful technique for mathematicians to formally verify and develop proofs. I will give an elementary introduction to the topic of ITP, explore the benefits of ITP for rigour, clarity, as well as collaboration in mathematical research and give an overview of the different available proof assistants. In the second part, I will showcase how to develop some simple (undergraduate level) theory using Lean, a user-friendly and versatile proof assistant with an active community and a large library of already implemented theories. This talk is introductory, no prior knowledge about ITP is assumed.