Formalising Mathematics (Imperial College London course)
by Bhavik Mehta (after Kevin Buzzard) · Imperial College London
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.
More resources on Formal Proof Assistants (Lean)
Theorem Proving in Lean 4
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.
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.