A guide to Lean — start here
Lean is a tool that has a machine check mathematical proofs. These pages cover what Lean is, how to use it on your own machine, how to build proofs in small examples, and how to make sure that a proof which passes the check actually says what you meant, in 14 pages.
Related: Principia (the list of articles) / The Lean verification bundle (the ledger of checked theorems and the distributed sources)
The pages
Start here (this page)
- What Lean is — propositions become types, proofs become terms. The kernel and tactics, the axioms, and what Lean does not guarantee
- Getting started — installing it and checking a single file. How to read errors and how to find lemmas
- Handing a finite check to
decide— turning "just count and see" into a computation by the kernel - Counting with
Finset— counting the elements of a finite set in a form you can prove things about - An upper bound from a single injection — when a two-line argument on paper is two lines in Lean as well
- Series and inequalities — closing an estimate of an infinite sum with the signs of the coefficients and the tools for convergence
- Having Lean check a certificate — search outside, and have the machine confirm only the answer that was found
- It passed — but does it say what you meant? — strong and weak definitions, what a theorem name covers, the list of hypotheses
- How to read a statement — what to check, and in what order, when you receive someone else's proof
- What is realistically too heavy for Lean — computational cost, theories not in stock, completeness that has no type. The criteria for deciding to leave something on paper
- Common pitfalls — where you get stuck, and what to do then
- Glossary — the 43 terms used in this guide, in 1–3 lines each
- How Lean works — where the idea of machine checking came from, how Lean itself is built, and what happens during a check
Where to start
You are seeing Lean for the first time
Read 01 → 02 → 03 in that order, and try checking the example in 03 on your own machine once. After that, take 04–07 in whatever order interests you. If a term stops you, go back to 12.
If you read the second half of 13 (how checking works) after 01, you can follow what happens during a check on a real example. Neither 01 nor 13 needs anything installed.
You want to know how to read a result that says "it passed in Lean"
08 → 09 → the last section of 01. Those three are enough. What a machine check guarantees and what it does not is at the end of 01; where exactly the things outside the guarantee show up is in 08; the procedure for the person receiving the proof is in 09.
The actual check results are in The Lean verification bundle. Theorem names, the axioms relied on, and the distributed sources are there.
You have a problem and are unsure whether to write it in Lean
10 → 11. 10 sorts the reasons for deciding not to write something into three kinds (cost, stock, completeness). 11 is the list of places where you get stuck once you have started writing.
The labels
Every claim in the articles on this site carries one of four labels. Lean is involved in the first one.
LeanMachine-checked. The check passes in Lean 4 with mathlib, the axioms relied on are within the three standard ones, and there is no hole from sorry and no native_decide. The theorem name is given
paperThere is a proof, but it has not been machine-checked
computationThe range confirmed by computation on our own machine. Not made into an outward claim
knownA rephrasing, a known theorem, or something confirmed in the outside literature
Why these four need to be told apart is explained at the end of 01. The Lean label says only that "this statement can be derived from the axioms"; it does not say that "this statement is what was meant".