SCO Seminar - Dr. Steffen Trenn, University of Groningen

Title: The future of math is here: The Lean theorem prover

Abstract:

During my PhD I became interested in the foundational basis of our modern mathematical theory: what are the underlying axioms and formal rules? And what exactly is the meaning and consequence of Gödel's incompleteness theorem? These questions are tightly connected with Whitehead and Russel's "Principia Mathematica" [1] which already provides a completely formalized (but mainly unreadable) foundation of mathematics. They were way ahead of their time, because without having a computer to reliably check each individual proof step, the formalization is still quite error prone. This problem was resolved about 30 years ago with the Metamath project [2] which formalized basic math results based on set theory, but it didn't gained much attraction. Recently I became aware of the lean theorem prover [3] and I think this is a game changer for how we do mathematics in the future.