Learn
Our most comprehensive materials to help you learn Lean.
Books & Manuals
The Lean 4 Manual Work-in-progress comprehensive overview of the language, including FAQs.
Functional Programming in Lean Standard reference for learning how to use Lean as a programming language.
Theorem Proving in Lean 4 Go-to resource for learning how to use Lean as a theorem prover.
Mathematics in Lean Learn how to use Lean for formalizing mathematics.
The Mechanics of Proof Instruction on how to write rigorous mathematical proofs, aimed at the early university level.
Additional Learning Resources The Lean community website hosts other useful tutorials and documentation sources for Lean 4.
Courses
The Lean Community’s hub for all past and current Lean courses.
Tools
Loogle Easily search Lean and Mathlib definitions and theorems.
Moogle Use Moogle to find theorems in Mathlib using natural language.
LeanDojo Python library designed for learning-based theorem proving in Lean.
Games
Lean Game Server Learn Lean through games, starting with the introductory Natural Number Game.