Lean 4 for mathematicians: a teacher's guide
Introduction
Who it is for. This guide is aimed at teachers who want to introduce Lean 4 to mathematics students who are used to writing proofs on paper but have no previous programming experience. No prior knowledge of computer science is required.
Philosophy of the course.
- Lean is a proof notebook that talks back. You write an argument and the computer tells you, step by step, what is missing. It is presented as a patient interlocutor, not as a programming language.
- Mathematics first, syntax later. Each topic starts from a proof the student already knows how to do on paper and translates it into Lean.
- No installation at the beginning. The first three sessions can be done in the browser. Local installation comes when the student already wants to carry on alone.
- You learn by reading the proof state. The central skill is not memorizing tactics, but reading the goals window (the infoview) the way one reads a blackboard.
- Making mistakes is cheap. The red error is information, not a failure.
Structure. Eight topics of about 2 hours each (theory and practice mixed). Each topic has two parts: the content (what the student sees) and the teaching tips (notes for the teacher with key ideas, typical mistakes, ...).
Convention. All the examples start with import Mathlib.Tactic, Lean's library of tactics. The code blocks can be pasted as they are into the editor.
| Topic | Title | Central idea |
|---|---|---|
| 1 | First contact | A theorem is a type; a proof is a term |
| 2 | Propositional logic | Connectives and the tactics that handle them |
| 3 | Quantifiers and sets | ∀, ∃, membership, inclusion |
| 4 | Equality and calculation |
rw, calc, ring, linarith
|
| 5 | Induction and recursion | Natural numbers, sums, recursive definitions |
| 6 | Your own definitions |
def, structure, limits |
| 7 | Finding your way around Mathlib | Looking up lemmas without knowing them by heart |
| 8 | Final project | Formalizing a result of your own |