Course Title: Introduction to Formal Proof Verification with Lean
Course Dates: March 10–21, 2025
Schedule: Monday to Friday, 9:30–12:30 and 14:00–17:00
Course Material: github.com/FordUniver/LeanBlockCourse
Lecturer: Christoph Spiegel
Exercise assistance: Olivia Röhrig
Course Description
This two-week block course introduces participants to formal proof verification using the Lean theorem prover. The focus is on practical engagement, with numerous examples provided. Participants are encouraged to follow along on their laptops during both lectures and tutorials.
General Notes
- This is the first time this course is being held. The structure is tentative and subject to change. Constructive feedback is welcomed throughout the course and afterwards.
- Lectures will behHeld in the lecture hall of the Zuse Institute Berlin (ZIB) and the rooms at Freie Universität Berlin (FU) for the tutorials will be decided once we have a better idea of the number of participants.
- The course is open to everyone, including guest auditors (Gasthörer), not just those who need it for their ABV modules. However, priority for tutorial sessions will be given to FU students who need the course as part of their degree program.
- Participants need to bring a laptop to do the exercises and follow along during lectures and tutorials.
- Completion of Analysis I and Linear Algebra I should provide a sufficient mathematical background, but participants should have a strong understanding of these subjects, as formal proof verification is very "unforgiving". No prior programming experience is required, but a certain "technical affinity and interest" is needed.
- The course will be conducted in English, but students may express themselves in German if they prefer.
All information about the course can be found on its github page.