Introduction to proof assistants

In this PhD Forum, we have Fellow EEMCS PhD candidate Kobe Wullaert, who will give us a short talk about proof assistants such as Lean, Isabelle, Coq (which will be the focus of the talk) - how and why they work, and how they can help us. Proof assistants take theorem statements and their proofs and translate them into machine-checkable terms thus verifying the validity of the proof. This exciting field connects mathematics and logical systems through programming, with both already established results verified, e.g. 99 out of “The Hundred Greatest Theorems”, and also taking part of cutting-edge mathematics, such as Scholze’s Analytic Geometry results.

We invite you to bring your own laptop if you would like to try to use the supercomputer following Dennis’ steps.

The event lasts around one hour and we will meet up at Labs for our customary free drinks and snacks afterwards.