Announcements
Mon, Mar 9New addendum: Prove axiom-free proofs — can you express within Lean's logic that a proof avoids a specific axiom?
Sun, Mar 8New addendum: theorem vs lemma.
Sun, Mar 8Updated P02 and P03 exercise files: named theorems are now example, with #check pointers to the corresponding Mathlib names. Use the Mathlib names in your proofs.
Sun, Mar 8New addendum: let vs have in tactic mode.
Thu, Mar 5New addendum: When · focusing is optional.
Thu, Mar 5New addendum: VS Code distractions.
Thu, Mar 5Since we went over by 10 minutes, the afternoon session starts at 14:10 instead of 14:00.
Wed, Mar 4New addendum: Proof length (#golf).
Tue, Mar 3Since we went over by 10 minutes, on Wednesday (March 4) we start at 9:40 instead of 9:30.
Mon, Mar 2Since we went over by 30 minutes, on Tuesday (March 3) we start at 10:00 instead of 9:30.
Mon, Mar 2Uploaded slides for P01_Introduction.

Formalized Math in Lean

Block Course at the Freie Universität Berlin — March 2026

This is the second time this course is being held. The structure will largely follow last year’s with some additions and modifications, but is nevertheless subject to (spontaneous) change. Constructive feedback is welcomed throughout the course and afterwards.

Teaching team

Christoph Spiegel will teach this course. He is a researcher at ZIB in Prof. Pokutta’s IOL group, working on combinatorics, optimization, machine learning, and proof formalization. Silas Rathke will serve as the teaching assistant. He is a Ph.D. student at FUB in Prof. Szabo’s group, focusing on extremal combinatorics and related formalization projects.

Time and venue

The course takes place from Monday the 2nd of March to Friday the 13th of March 2026, split into two daily sessions (9:30–12:30 and 14:00–17:00). It will be held in Seminarraum 119 (A3/SR 119) at Arnimallee 3 on the FUB Dahlem Campus.

Registration and credit

The course is open to everyone, including guest auditors (Gasthörer), not just those who need it for their degree. Priority will be given to FU students who need the course as part of their ABV degree program. The course will also be offered for Master students at the FUB as well as a BMS Advanced Course for the first time this year!

For the aktive Teilnahme, Master-level participants will be required to solve additional and more advanced problems in the exercise sessions compared to Bachelor-level students. Both Bachelor and Master-level students will sit the same final exam on the second Friday. Master-level students will additionally receive a small formalization project to complete in the one or two weeks following the course. The exact scope and evaluation format has not yet been determined but may include an in-person presentation.

Prerequisites

Completion of Analysis I and Linear Algebra I should provide a sufficient mathematical background, though participants should have a strong command 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. Besides formal proof verification, you will be in contact with many other tools such as git and GitHub, Patrick Massot’s leanblueprint, CI/CD in the form of GitHub Actions, as well as various ML tools.

Participants need to bring a laptop to follow along and work on exercises. The course will be conducted in English, but Bachelor students taking the course as part of their ABV requirements may express themselves in German if they prefer.

  • Course Outline — parts, sections, slides, and exercises
  • Setup — installation, project creation, and troubleshooting
  • Unicode Input — backslash commands for all symbols used in the course
  • Tactic Reference — every tactic used in the course, by section
  • Resources — textbooks, documentation, talks, and games
  • Addendum — follow-ups and clarifications from the lectures
This site uses Just the Docs, a documentation theme for Jekyll.