Interactive Theorem Proving in Lean
Florent Schaffhauser, Heidelberg University
Topic and goal
Programming languages with strong type-checking capabilities can be used to represent abstract mathematical objects, state theorems about them, and write formal proofs. In this workshop, we explore the world of proof assistants and formal mathematics using Lean 4, a relatively recent functional programming language with a rapidly growing mathematical library. The goal is to help mathematicians develop new coding skills while becoming acquainted with formal methods in their field.
Organization of the lectures
We give an 8h introduction to certified programming and formal mathematics aimed at graduate students interested in the interaction between mathematics and computer science. Each session will combine a lecture with hands-on computer practice.
Participants are encouraged to work in pairs. Practice files for each session will be provided and no prior installation of Lean is required.
| Lecture | Topic | Practice files |
|---|---|---|
| 1 | An introduction to Lean | |
| 2 | Basic tactics | |
| 3 | Dependent types | |
| 4 | Algebraic structures |
Audience questions
Answers to some of the questions from the audience are available here:
- Lecture 1: How to declare a function
- Lecture 2: How to pass the constructors of an inductive type
Design & Build
This webpage is produced using Quarto Markdown and VS Code. The slides are produced using Marp, also within VS Code. The website is published via GitHub Pages. The QR codes are generated using Python’s qrcode package.