Theorem Proving in Lean 4
by Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich · Lean FRO
Official Lean 4 text on the underlying logic. It covers dependent type theory, propositions as types, quantifiers, equality, inductive types, structures, type classes, tactics, well-founded recursion, and the axioms Lean adds, with how they affect computation. This is the primary source for the dependent type theory part of the topic. It complements Mathematics in Lean, which focuses on practice rather than foundations.
More resources on Formal Proof Assistants (Lean)
Formalising Mathematics (Imperial College London course)
Imperial College London's undergraduate course on formalising mathematics in Lean 4 and Mathlib. It provides graded exercise sheets on logic, sets, functions, groups, limits, topology and more, with a tactics handbook, and runs locally or in-browser via Codespaces or Gitpod.
Mathematics in Lean
Free, continuously updated Lean 4 and Mathlib textbook with exercise files. Its 13 chapters run from logic, sets and functions through elementary number theory, structures, groups and rings, linear algebra, topology, differential calculus, and integration and measure theory.
The Mechanics of Proof
Free online introduction-to-proofs textbook that pairs each argument with a Lean 4 formalisation. It covers computation, parity, divisibility, modular arithmetic, induction, functions, sets and relations, with a tactic index. Written for Fordham's Math 2001.
Natural Number Game (Lean 4)
Browser-based puzzle game in which you build the natural numbers from Peano's axioms and prove addition, multiplication and ordering facts in Lean 4, one tactic at a time. It needs no installation and is the usual first contact with Lean.