Interactive Theorem Proving in Lean
Florent Schaffhauser, Heidelberg University
General information
- Compact course at the Heidelberg Graduate School of Mathematical and Computational Methods for the Sciences (HGS MathComp).
- Target audience: Graduate students of the Faculty of Mathematics and Computer Science at Heidelberg University.
- Instructor: Florent Schaffhauser.
Topic and goal
Producing certified, reliable code is crucial in software engineering. Taking it a step further, modern programming languages with strong type-checking capabilities can even be used to state theorems about abstract mathematical objects and verify the correctness of proofs.
In this workshop, we explore the world of proof assistants and learn how to explain mathematics to a computer using Lean. The goal is to help participants develop new coding skills while becoming acquainted with formal methods on a larger scale.
Organization of the lectures
We give an 8h introduction to certified programming and formal mathematics for 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.