5.1. Slides🔗

Most chapters have a deck, used in the lecture and readable on its own. The figures and claims are those of the text, so either can be used without the other.

• Why formalize? — the first lecture: what formalizing means, where things stand in 2026, the four episodes and the landmark formalizations.

• The natural numbers and reduction rules — chapter 1.1

A deck appears here when its chapter is taught.

Press s in a deck for the speaker notes, o for an overview of all slides, and ? for the remaining keys. Every slide carries a link in its upper right corner that leads back to this page.

5.2. Recordings🔗

The lectures and lab sessions are recorded and published on Formally proven, the course's YouTube channel. Each recording carries chapter marks that follow the slides, so a single topic can be found without watching the whole hour.

5.3. What comes when🔗

Sheets are named after the chapter they belong to, so 2.6-b is the second sheet on chapter 2.6. L-a to L-g are the logic block, which belongs to no chapter and runs alongside the first five weeks; A-a and A-b are the appendix, X-a an extra sheet.

Each week has two rows: the lecture on Monday presents a chapter, the lab on Wednesday works on the sheets of that week. The short tests are written at the start of the lab.

5.4. The short tests🔗

Five tests, 20 minutes each, at the start of the lab, on paper. Three of the five must be passed for the Studienleistung. A test is passed when 50% of all points are achieved. A test not taken counts as not passed.

Dates: 11.11., 02.12., 16.12., 27.01., 10.02.

What is tested is the proof state and understanding. Here are some typical questions:

• The state is h : P ∧ Q, the goal ⊢ R. You write obtain ⟨hP, hQ⟩ := h. What does the state look like afterwards?

• Is ¬(P ∧ Q) → (¬P ∨ ¬Q) provable constructively? If not, where does the excluded middle come in?

• This proof fails with "no binders to introduce". Why?

5.5. Goals🔗

The course is for mathematics students.

• Reading formal statements. Judging whether a formal statement says what the informal one claims (see above).

• Interactive theorem proving. A small kernel checks every logical step of a proof, and the editor reports what remains to be proved as you write (the proof state). This is not the older use of computers in mathematics, which was to work through many cases (the four colour theorem).

• Mathematical content. The mathematics in the first half is deliberately easy, because explaining a proof to a computer requires understanding it first, and a proof of more than a few lines has to be planned so that the commands — tactics — fit together. The second half goes deeper into the mathematics.

• Functional programming. Inductive types, structures, typeclasses and monads, needed both to use Lean and to read Mathlib.

• Type theory. Lean rests on dependent type theory: the Curry-Howard correspondence, dependent types, the universe hierarchy, and Lean's axioms.

• Mathematics in Mathlib. How the library organizes order theory, the algebraic hierarchy, filters (a single framework for limits), topology, measure theory and discrete probability. Textbooks rarely treat these from the point of view of formalization.

• Proof engineering. Automation tactics, searching Mathlib, and the common pitfalls of a large formal library.

5.6. Getting Lean running🔗

Hardware. Lean memory-maps all of Mathlib while it works, and every exercise sheet begins with import Mathlib. A two-line sheet therefore needs as much memory as the hardest one in the course.

Most of the RAM requirement comes from memory-mapped library data, which the system can drop and read back from disk, so less memory does not break anything, it only slows everything down by a large margin.

If your machine is below the minimum, talk to the teachers at the start of the course. A server with 128 GB of RAM is available and we can give you an account on it.

Run the git clone and lake exe cache get below at home: lake exe cache get downloads several gigabytes, and twenty people doing that at once on one network is slow for all of them.

• Install VS Code.

• Open VS Code, hit the extensions icon (fifth from the top) on the left, and install the Lean 4 language extension.

• Install git, if you do not have it: open VS Code, hit the git icon (third from the top on the left), and follow the instructions.

• The exercises repository. Go to where you want the course materials and run

git clone https://github.com/pfaffelh/leancourse_exercises
cd leancourse_exercises
lake exe cache get
code .

VS Code opens with the course materials. (These notes are generated from a second repository, pfaffelh/leancourse, which you do not need to clone.)

After code . in the leancourse_exercises folder, open Exercises/0-Logic/a-Propositions.lean. It works once the orange and red bars disappear and moving the cursor on the left changes the infoview on the right. Then copy the Exercises directory to MyExercises and work there. To get updates, run git pull in leancourse_exercises. MyExercises is ignored by git, so an update never overwrites your files.

If the installation gives you trouble, talk to the teachers.

5.7. How these notes are organized🔗

The notes have six parts.

• Lean and its type theory: the natural numbers and reduction, types, terms, typeclasses, propositions as types, dependent types and notation.

• Mathematics: sets and types, universes and axioms, well-foundedness, then the areas of Mathlib listed above. Pointers into the API, not full formalizations.

• Appendix: the glossary of tactics (a longer list is here), the structure of a Lean file, navigating Mathlib, common pitfalls, and small reference topics such as the diagnostic commands (#print axioms, #find_home, #lint).

• Projects: five topics for the individual formalization projects, each with a description, a sketch of an implementation and references.

• Bibliography: the works cited throughout, with links.

• Organization: what comes when, the short tests, the slides and the recordings.

Tactics and theory are interleaved. You usually meet a tactic in a working example before you read its entry in the glossary, which is meant for looking things up, not for reading in order. The cheatsheet lists the tactics needed first.

The exercises carry the course (the Exercises folder of the exercises repository, see below). Feedback is immediate: error messages from the elaborator, and the proof state in the infoview, which shows what remains to be proved at every cursor position. Start with the first sheet; the sheets explain as they go.

In addition to the sheets, you work on an individual project, mostly self-chosen — an exercise from your first year, or a part of Mathlib you want to know; the Projects chapter has five worked-out suggestions.

Before the first lab session, get Lean running on your own machine.