Table of contents

Lean from First Proofs to Formalized Mathematics

A visual, complete learning path from programming fundamentals to expert theorem proving in Lean

Read each section in order. Every title can be opened as a TheoryTrace document.

• Cover
• Copyright
• How to read this book
• Introduction
• Chapter 1: What Lean Is and How Formalization Changes Mathematics
• Chapter 2: Setting Up a Lean Working Environment
• Chapter 3: The First Lean Terms, Types, and Commands
• Chapter 4: Propositions as Types and Proofs as Terms
• Chapter 5: The Calculus of Dependent Types
• Chapter 6: Quantifiers, Equality, and Rewriting
• Chapter 7: Defining Data with Inductive Types
• Chapter 8: Recursive Definitions and Termination
• Chapter 9: Pattern Matching, Functions, and Computation
• Chapter 10: Structures, Records, and Mathematical Objects
• Chapter 11: Type Classes and Instance Synthesis
• Chapter 12: Notation, Syntax, Macros, and Elaboration
• Chapter 13: Namespaces, Modules, Imports, and Large Projects
• Chapter 14: The Tactic Mode Mental Model
• Chapter 15: Core Interactive Tactics for Logic and Equality
• Chapter 16: Simplification, Normalization, and Automation
• Chapter 17: Attributes, Declarations, and the Lean Environment
• Chapter 18: Coercions, Subtypes, Quotients, and Extensionality
• Chapter 19: Universes, Sorts, and Foundational Boundaries
• Chapter 20: Classical Reasoning and Constructive Reasoning
• Chapter 21: Searching, Reading, and Reusing Mathlib
• Chapter 22: Sets, Relations, Functions, and Basic Discrete Mathematics
• Chapter 23: Algebraic Hierarchies in Lean
• Chapter 24: Order, Lattice, and Topological Interfaces
• Chapter 25: Analysis and Calculational Proof in Mathlib
• Chapter 26: Induction, Recursion, and Well-Founded Proofs at Scale
• Chapter 27: Metaprogramming Foundations in Lean
• Chapter 28: Writing Custom Tactics and Proof Automation
• Chapter 29: Software Engineering for Formalization Projects
• Chapter 30: Debugging Lean Proofs and Understanding Error Messages
• Chapter 31: Designing Visual Demonstrations for Every Lean Feature
• Chapter 32: Case Study I — Formalizing a Complete Discrete Mathematics Development
• Chapter 33: Case Study II — Building an Algebraic Theory
• Chapter 34: Case Study III — A First Formal Analysis Project
• Chapter 35: From Competence to Mastery
• Conclusion