Lean theorem prover/Applications/Teaching with Lean

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

Lean is used to teach mathematical proof, the logic behind it, and programming. This page describes the main free materials, from a puzzle game for beginners to textbooks for undergraduates and researchers, and some university courses built on them. It also says what a proof checker adds to teaching and what it does not.

What a proof checker gives a learner

A student writing a proof on paper waits for a teacher to mark it. A student writing a proof in Lean is answered at once: each step is accepted, or refused with the goal that is still open (see Holes and goals). The checker never tires, and it does not accept a step because it looks plausible. It cannot tell a student whether a proof is well written or why it works; those remain the teacher's work.

The Natural Number Game

The Natural Number Game is a browser game that teaches the first steps of proof in Lean. It starts from a definition of the natural numbers made from zero and a successor operation, and asks the player to prove facts about them in order: first that 2 + 2 = 4, then that $x+y=y+x$, and so on through a sequence of "worlds", each made of levels that are theorems.

The game was written for Lean 3 by Kevin Buzzard and Mohammad Pedramfar. Its Lean 4 version is credited to Buzzard and Jon Eugster, on a game engine by Alexander Bentkamp, Eugster and Patrick Massot. It runs on the Lean Game Server, which also hosts games maintained by other authors, among them a set theory game (Dan Velleman), a real analysis game (Alex Kontorovich) and Reintroduction to Proofs (Emily Riehl).

A small piece in the game's style shows the idea. The natural numbers are defined from scratch, addition is defined by recursion on its second argument, and adding zero on the left then needs a proof by induction:

inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat

namespace MyNat

def add : MyNat → MyNat → MyNat
  | a, zero   => a
  | a, succ b => succ (add a b)

/-- Adding zero on the right is the definition; on the left it needs induction. -/
theorem zero_add (n : MyNat) : add zero n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [add, ih]

end MyNat

Lean 4.34.1 accepts it. A beginner who offers rfl as the whole proof is refused: Lean reports that the left-hand side, zero.add n, is not definitionally equal to the right-hand side, n. The definition of addition says nothing directly about add zero n while n is unknown. That refusal is the point at which induction is learned. The explainer Induction, as the machine sees it says more.

Textbooks

The standard free books are published by the Lean community and the Lean developers.

• Theorem Proving in Lean 4, by Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, with contributions from the community, teaches Lean's logic itself: dependent type theory, propositions and proofs, tactics, inductive types, structures, type classes and the axioms.
• Mathematics in Lean, by Avigad and Patrick Massot, teaches how to do mathematics with Mathlib, in chapters running from basic logic and number theory through structures, algebra and linear algebra to topology, differential calculus, and integration and measure theory.
• Functional Programming in Lean, by David Thrane Christiansen, is a free book on Lean as a programming language, from its basics through type classes, monads and dependent types to proofs about programs and performance.
• Logic and Proof, written by Avigad, Lewis and van Doorn and adapted to Lean 4 by Hua, is an introduction to symbolic logic and mathematical proof. Its stated goals are that a reader learn to write clear proofs, to model deductive proof formally, and to use an interactive proof assistant.

University courses

Two published course texts show Lean in use at different levels.

• The Mechanics of Proof, by Heather Macbeth, was written for the course Math 2001 at Fordham University and is aimed at the early university level. It describes itself as a book about writing careful, rigorous proofs, and it is paired with Lean code throughout, with an appendix on moving on to mainstream Lean.
• Formalising Mathematics, by Kevin Buzzard, is the handbook for his course of that name at Imperial College London, aimed at students with some mathematical background, such as those in the final year of a mathematics degree. It teaches how to formalise mathematics in Lean using Mathlib, and includes a catalogue of basic tactics.

Courses are offered elsewhere too; this page lists only those whose published materials could be checked.

How quickly mathematicians learn

The authors of the formalisation of perfectoid spaces reported that mathematicians without training in computer science can become proficient with a proof assistant within a short time. Buzzard hoped that his Fermat project would be a good source of smaller Lean projects for doctoral students in number theory who want to learn the language.

What it does not teach

Lean checks that a proof is correct. It does not show which proof is clearest, and a proof written for Lean can be longer and harder to read than one written for people. Course texts such as Macbeth's present themselves as books about writing careful, rigorous proofs, with Lean as the companion that checks them. The gap between a proof that Lean accepts and a proof a reader understands is discussed in Checking instead of convincing.

Next

• Machine learning and theorem proving.
• What a proof assistant does, for a reader starting from the beginning.