A Practitioner’s Guide to the Lean Book Landscape

Lean has matured from a research prototype to a full‑featured proof assistant with a growing ecosystem of textbooks, tutorials, and interactive games. The market is now cluttered with titles that promise to teach “Lean from scratch,” yet many of them overlap heavily or target very narrow use‑cases. Below I break down the most referenced resources, point out what is genuinely new in each, and flag the practical limits you’ll hit if you try to read them all at once.

---

1. What’s actually new?

Resource	Primary focus	New content compared to the rest	Typical audience
Functional Programming in Lean (David Thrane Christiansen)	Lean as a general‑purpose functional language	First book that treats Lean like a programming language rather than a proof assistant; thorough coverage of structures, type classes, and instance search	Beginners who want to write non‑tactic code, or developers transitioning from Haskell/OCaml
Metaprogramming in Lean (Arthur Paulino et al.)	Writing tactics, extending the compiler, VS Code integration	Only dedicated tutorial on Lean‑4 metaprogramming; includes hands‑on exercises that culminate in a simple tactic library	Users planning to contribute to Mathlib, build custom tactics, or work on the Lean core
The Hitchhiker’s Guide to Logical Verification (Baanen, Bentkamp, …)	Theory‑first introduction, bottom‑up vs top‑down proof styles	Provides a concise, example‑rich treatment of type‑theory judgments and a clear explanation of why Lean’s tactic language behaves the way it does	Readers who already know a proof assistant and want a quick theoretical refresher
Theorem Proving in Lean (Avigad, de Moura, Kong, Ullrich)	End‑to‑end walkthrough from proof terms to tactics	Deep dive into inductive definitions, recursors, and the Calculus of Constructions with inductive types; written by the original Lean developers	Anyone seeking a comprehensive, language‑centric reference
Mathematics in Lean (Avigad, Massot)	Formalising mainstream mathematics using Mathlib	Hands‑on series of theorems that mirror a standard undergraduate curriculum; fast‑paced but realistic for Mathlib contributors	Mathematicians who intend to contribute new results to Mathlib
Logic and Proof (Avigad, Lewis, van Doorn)	Logic textbook with Lean interleaving	Alternates pure logic chapters with Lean implementations, reinforcing each concept twice	Students with a background in undergraduate logic who want to see the formalisation side by side
Natural Number Game (Buzzard, Pedramfar)	Interactive tutorial/game	Gamified introduction to inductive types and basic proof tactics; works in both Lean 3 and Lean 4	Absolute beginners; also a good warm‑up before any textbook
Formalising Mathematics (Buzzard)	Course‑style repo for PhD‑level formalisation	Extends the Natural Number Game to genuine mathematical development; more theorems, deeper libraries	Advanced students aiming for research‑level formalisation
Logic and Mechanized Reasoning (Avigad, Heule, Nawrocki)	Logic + SAT/SMT implementation in Lean	Implements propositional and first‑order logic solvers from scratch; not a tactic‑writing guide but a concrete example of using Lean as a programming language
Lean Language Manual (Lean 3/Lean 4)	Reference documentation	Lean 3 manual is readable as a book; Lean 4 version is more a collection of notes and API docs
How to Prove It with Lean (Velleman)	Planned adaptation of classic proof‑technique textbook	Not yet released; expected to map classic textbook exercises onto Lean
The Mechanics of Proof (Macbeth)	Course notes for a university class	Targeted at students with strong mathematical background but new to formalisation
Lean‑4 Tactic Writing Tutorial (Sedláček)	Short tutorial on tactic implementation	Companion piece to Metaprogramming in Lean; not a full book

What you won’t find duplicated

• A single source that covers both Lean‑4 metaprogramming and deep mathematical libraries. The closest is the combination of Metaprogramming in Lean + Mathematics in Lean.
• A beginner‑friendly, narrative‑style textbook that treats Lean as a programming language. Functional Programming in Lean fills this gap, but it assumes you are comfortable with functional programming concepts already.
• A systematic treatment of Lean’s elaboration and metavariable solving. The relevant material lives scattered across Theorem Proving in Lean and the source code of the Lean kernel.

---

2. Practical limitations

1. Version fragmentation – Many older titles (e.g., the original Lean 3 language manual, Theorem Proving in Lean first edition) target Lean 3. While most concepts transfer, syntax differences (especially around simp lemmas, match syntax, and the new by block) can cause confusion for newcomers who only have Lean 4 installed.
2. Depth vs. breadth trade‑off – Books such as Logic and Proof interleave theory and code, which is excellent for reinforcement but slows progress if you simply want to write proofs. Skipping the theory chapters is possible, but you lose the intuition that later Mathlib development relies on.
3. Exercise support – Only a handful of resources provide automated test harnesses (e.g., the Natural Number Game, the exercises in Metaprogramming in Lean). The rest are pure PDFs; you must manually copy code into a Lean project, which can be tedious and error‑prone.
4. Community maintenance – Some repos (e.g., Formalising Mathematics) are updated irregularly. If you depend on the latest Mathlib, you may need to patch the examples yourself.
5. Print vs. digital – The author of the original list mentions printing 250‑page PDFs for mental separation. While this works for some, the Lean ecosystem evolves quickly; printed copies become stale, especially for Lean 4‑only material.

---

3. Suggested learning pathways

Below is a condensed version of the “forking paths” table, reorganised by the minimum prerequisite knowledge each path assumes.

3.1 If you already know a proof assistant (Coq, Isabelle, …)

1. Theorem Proving in Lean – solidifies Lean‑specific syntax and the underlying type theory.
2. Choose a domain‑specific follow‑up:
   • Mathematics in Lean for Mathlib work.
   • Metaprogramming in Lean if you plan to write tactics.
   • Logic and Mechanized Reasoning for a deeper logic implementation project.

3.2 If you are a software developer curious about Lean as a language

1. Functional Programming in Lean – get comfortable with structures, type classes, and the IO monad.
2. Theorem Proving in Lean – learn the proof‑term ↔ tactic bridge.
3. Metaprogramming in Lean – optional, only if you need custom tactics.

3.3 If you are a mathematician with no prior proof‑assistant exposure

1. Natural Number Game – 30‑minute interactive intro.
2. Functional Programming in Lean – optional, but helps demystify the syntax.
3. Theorem Proving in Lean – establishes the proof workflow.
4. Mathematics in Lean – start formalising undergraduate‑level theorems.
5. Logic and Proof – optional, for a formal logic refresher.

3.4 If you want to contribute to Mathlib

1. Mathematics in Lean – learn the style of Mathlib proofs.
2. Theorem Proving in Lean – fill any gaps in language knowledge.
3. Metaprogramming in Lean – understand the macro system used by many Mathlib contributors.
4. Logic and Mechanized Reasoning – optional, but gives insight into how Lean can be used for algorithmic logic.

---

4. How to make the most of the books

• Clone the associated GitHub repos rather than relying on PDFs. Most authors keep the source files in a src/ folder that you can open directly in VS Code with the Lean extension.
• Run the exercises in watch‑mode (lean --run) so you get immediate feedback on missing lemmas.
• Use Paperproof or a similar animation tool to visualise tactic state changes; this is especially helpful for Metaprogramming in Lean where the internal goal stack can be opaque.
• Keep a small “cheat sheet” of Lean‑specific syntax differences (e.g., simp vs simp_all, match vs cases) as you move between Lean 3‑centric books and Lean 4‑only material.
• Participate in the community Discord or Zulip; many of the authors (e.g., Jannis Limperg, Jeremy Avigad) answer questions in real time, which reduces the feeling of reading a static textbook.

---

5. What’s missing and where to look next

• A systematic treatment of Lean’s elaboration pipeline – currently only scattered in the source code and a few blog posts.
• A beginner‑friendly guide to the new by‑style proof syntax – the community is working on a short tutorial, but it is not yet packaged as a book.
• More extensive coverage of the Lean‑4 standard library – the official docs are improving, yet a textbook‑style walkthrough would help newcomers avoid “search‑the‑repo” fatigue.

If you discover a new resource (a blog series, a university lecture repo, or a well‑maintained set of exercises), feel free to open a PR on the original list’s repository or drop a comment on the Lean Zulip channel.

---

TL;DR

• Read Functional Programming in Lean first if you need language basics.
• Read Theorem Proving in Lean next; it is the only comprehensive, language‑level reference.
• Pick Metaprogramming in Lean only when you need to write tactics.
• Use the game‑based resources (Natural Number Game, Formalising Mathematics) as low‑friction entry points.
• Supplement with domain‑specific books (Mathematics in Lean, Logic and Proof) based on your goals.

By following a focused path instead of trying to consume every PDF, you’ll avoid redundant chapters, keep your Lean installation up‑to‑date, and build a practical skill set that translates directly into Mathlib contributions or custom tactic development.