---
title: Formal Proof Assistants (Lean)
description: Proof assistants check mathematics by computer. You will learn Lean and dependent type theory, formalising definitions and theorems, and how the mathlib community is building a verified library of mathematics.
category: mathematics
subcategory: mathematical-logic
difficulty: beginner, intermediate, advanced
url: /subject/formal-proof-assistants-lean
---

# Formal Proof Assistants (Lean)

Proof assistants check mathematics by computer. You will learn Lean and dependent type theory, formalising definitions and theorems, and how the mathlib community is building a verified library of mathematics.

## Available Resources

3 Books • 1 Courses • 1 Websites

## Courses

### 1. Formalising Mathematics (Imperial College London course)

**Author:** Bhavik Mehta (after Kevin Buzzard)

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.

**Difficulty:** Intermediate | **Language:** English | **Price:** Free

**Link:** https://github.com/b-mehta/formalising-mathematics-notes

**Tags:** lean4, mathlib, formalization, interactive-theorem-proving, proof-tactics

## Books

### 1. Theorem Proving in Lean 4

**Author:** Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich

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.

**Difficulty:** Advanced | **Language:** English | **Price:** Free

**Link:** https://lean-lang.org/theorem_proving_in_lean4/

**Tags:** lean4, dependent-type-theory, propositions-as-types, interactive-theorem-proving, inductive-types

### 2. Mathematics in Lean

**Author:** Jeremy Avigad, Patrick Massot

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.

**Difficulty:** Intermediate | **Language:** English | **Price:** Free

**Link:** https://leanprover-community.github.io/mathematics_in_lean/

**Tags:** lean4, mathlib, formalized-mathematics, interactive-theorem-proving, proof-tactics

### 3. The Mechanics of Proof

**Author:** Heather Macbeth

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.

**Difficulty:** Beginner | **Language:** English | **Price:** Free

**Link:** https://hrmacbeth.github.io/math2001/

**Tags:** lean-4, intro-to-proofs, formal-verification, induction, number-theory

## Websites

### 1. Natural Number Game (Lean 4)

**Author:** Kevin Buzzard, Jon Eugster

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.

**Difficulty:** Beginner | **Language:** English | **Price:** Free

**Link:** https://adam.math.hhu.de/#/g/leanprover-community/nng4

**Tags:** lean-4, peano-axioms, natural-numbers, interactive-theorem-proving, tactics

---

*This content is part of Dantes.io - Your Treasure Map to Knowledge*

*Curated by humans at Dantes.io. Personal study use welcome; republishing this curation requires permission (team@dantes.io).*

View this page online: https://dantes.io/subject/formal-proof-assistants-lean