Lean in Mathematics and AI

Overview

Lean is a language for writing mathematical proofs that a computer checks line by line, and Mathlib is its library of formalized mathematics, from linear algebra to measure theory. In this seminar we learn to use them, and each participant formalizes problems from the department's qualifying exams. No prior Lean or type theory is needed.

There is no grading. The seminar ends with participants presenting their formalizations to each other.

We meet one hour a week, and most of the work happens at home. Each week has reading and exercises, listed in the schedule below; the exercise files are in the seminar's GitHub repository. The meetings are for live demos, getting unstuck, and looking at each other's proofs.

Why qualifying-exam problems? In recent tests, the best AI systems produced no valid Lean proof of any algebra problem at qualifying-exam level (FATE), and proved at most 1% of such problems in analysis (MA-ProofBench). A formalized qualifying-exam problem is something current AI systems cannot produce on their own.

Before the first meeting

1. Install Lean. Install VS Code and its Lean 4 extension by following the official instructions. You need about 10 GB of free disk space; 16 GB of memory is comfortable. No suitable computer? You can work in the browser instead, with the Open in GitHub Codespaces button in the seminar repository.
2. Get the seminar repository. With a GitHub account, make your own copy of the repository (the Fork button), then in a terminal:

   git clone https://github.com/YOUR-GITHUB-NAME/lean-seminar.git
   cd lean-seminar
   lake exe cache get

   The last command downloads Mathlib already compiled. Do not skip it: without it, Lean compiles all of Mathlib itself, which takes hours. Then open the lean-seminar folder in VS Code. The repository's README has the details, including how to get each week's new exercises.
3. Play the Natural Number Game through at least World 4. It runs in the browser.
4. Watch and type along with Alex Kontorovich's How Mathematicians can Get Started with Lean (32 minutes), in the file Exercises/Week00_Squeeze.lean. He proves the squeeze theorem, but the video stops before the proof is finished. Finishing it is your first exercise.

Things that trip up beginners

• The lines of a proof after by must be indented. Use spaces: Lean rejects tab characters.
• Symbols are typed with backslash codes: \R gives ℝ, \N gives ℕ, \to gives →, \e gives ε, \< gives ⟨. The code turns into the symbol when you type a space after it.
• Powers are written x ^ 2; Lean does not understand x².
• Names of hypotheses, like h or n_gt_N, are labels you choose. Lean never reads them; the meaning comes from the statement.
• If the goals shown seem to stop partway through a proof, look for an error above that point: after a syntax error, Lean skips the rest of the proof.
• The goals appear in VS Code's Lean Infoview panel. Cmd+Shift+Enter (Ctrl+Shift+Enter on Windows and Linux) shows or hides it.

How the seminar works

• Meetings take one hour: about 20 minutes of live demo of the week's topic, 30 minutes on problems people hit at home, and 10 minutes previewing the next week.
• At home you do the week's reading and exercises, listed in the schedule. New exercise files appear in the repository's Exercises folder each week.
• Questions go to the Discussions board, whenever you are stuck; do not wait for the meeting. For general Lean questions, the Lean community's Zulip chat answers fast, especially the channels #new members and #Is there code for X?
• Your project starts in week 11: you formalize problems of your choice from the department's qualifying exams (see Projects below), and present your work in week 13 or 14.

Schedule

MiL is Mathematics in Lean, a free online book with exercises built in.

Projects

From week 11 you formalize problems from the department's qualifying exams. What is hard on paper and what is hard in Lean are different things, so choosing a problem matters as much as solving it.

• Easy in Lean, hard on paper: problems whose theorem Mathlib already has in the right generality. A finite $p$-group has nontrivial center; the Sylow theorems; Cayley–Hamilton; dominated convergence. These take a few lines.
• Routine on paper, expensive in Lean: classifying the groups of order 12; computing a Jordan form (Mathlib has no Jordan normal form); evaluating one specific contour integral; computing the homology of the Klein bottle. In Lean, a general theorem is often easier than one specific instance.
• Good projects sit in between: the objects are in Mathlib, but the argument is more than one lemma. For example Noetherian and Artinian rings, integral extensions and going-up, flatness criteria, discrete valuation rings, $L^p$ duality, or the Galois group of a specific polynomial.

Choose a scope

• Breadth: three or four problems proved, at the level of textbook exercises.
• Depth: one or two harder problems proved.
• Library-building: one problem that needs at least one new definition, with the lemmas to use it. This is beyond what current AI systems can do.

The feasibility check, week 11

Before committing to a problem, work through five things:

1. A Lean statement of the problem that compiles, with sorry as its proof.
2. Each object in the statement, with its name in Mathlib. Note anything Mathlib does not have.
3. An example that satisfies all the hypotheses, so the statement is not vacuous.
4. For each partial operation in the statement, like division, subtraction of natural numbers or logarithms: one line on why Lean's convention at the boundary does not change the meaning. (In Lean, $x/0 = 0$ and $3 - 5 = 0$ in $\mathbb{N}$.)
5. Three Mathlib lemmas you expect to use.

Start from Seminar/ProjectTemplate.lean; the repository's Projects/README.md explains where to put your files. Then post the check with the Feasibility check form under the repository's Issues. If a problem fails one of the five, that is worth knowing early: we will help you rescope it or choose another.

Presentations

In weeks 13 and 14, each participant gives a talk of 20–25 minutes, including questions. A talk shows:

• the Lean statement next to the exam's wording;
• what formalizing made you decide: what the problem left implicit, where the Lean statement differs from the exam's wording and why that is harmless, and what formalizing revealed about the proof;
• the proof, with #print axioms for each main theorem;
• anything not finished yet. An honest partial result makes a good talk.

Before your talk, add your project to the repository with a pull request. scripts/check.sh in the repository tells you whether a proof is really finished: Lean accepts a file containing sorry with only a warning.

Talks

To be announced.

Resources

Books

• Mathematics in Lean, by J. Avigad and P. Massot. The main text.
• Theorem Proving in Lean 4, by J. Avigad, L. de Moura, S. Kong and S. Ullrich. For looking up how Lean itself works.
• The Mechanics of Proof, by H. Macbeth. Gentler and slower, if the first weeks feel fast.

Finding lemmas

• Mathlib documentation — browse everything in the library.
• Loogle — search by the shape of a statement.
• LeanSearch and Lean Finder — search in plain English.
• The Lean language reference — including an index of all tactics.

Problems and papers

• FATE — algebra problems stated in Lean, from textbook to qualifying-exam level.
• MA-ProofBench — the same for analysis.
• FormalProofBench, SorryDB, Aristotle, Lean Finder — papers for week 10.
• J. Avigad, Mathematics and the formal turn — why formalization matters to mathematicians.