Resources

Documentation and Search

• Mathlib documentation — official docs for the Mathlib library
• LeanSearch — natural-language search over Mathlib

Textbooks

• Theorem Proving in Lean 4 by Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich
• Mathematics in Lean by Jeremy Avigad and Patrick Massot
• The Hitchhiker’s Guide to Logical Verification by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, Jannis Limperg
• The Mechanics of Proof by Heather Macbeth
• Functional Programming in Lean by David Thrane Christiansen

Talks

• Kevin Buzzard: The rise of formalism in mathematics (ICM 2022)

Interactive

• Lean Game Server — inspired many of the smaller exercises in this course