Introduction

Mathematics has always depended on proof, but most mathematical proof is written for human readers. A journal proof, a blackboard proof, or a proof in a textbook is usually a carefully compressed argument: it says enough for a trained reader to reconstruct the missing steps. A formal proof is different. In a formal proof, the definitions, statements, and reasoning steps are written in a precise language so that a computer can check whether each step follows from earlier ones. Lean is one of the modern systems built for this purpose: it is both a programming language and an interactive theorem prover based on dependent type theory, with a small trusted kernel that checks elaborated terms (de Moura et al., 2015; Lean FRO, 2025).

This book is about learning Lean from the beginning, but not merely as a tool for solving isolated exercises. The goal is to learn Lean as a working language for formalized mathematics: a way to define mathematical objects, state theorems about them, construct proofs, reuse large libraries, automate routine reasoning, and eventually contribute reliable formal developments of your own.

We will move slowly at first. Then we will move deeply.

You are assumed to know basic programming ideas such as functions, variables, expressions, and data. You are also assumed to know the basic connectives of propositional logic: “and”, “or”, “implies”, “not”, “true”, and “false”. You are not assumed to know axiomatization, type theory, category theory, proof assistant architecture, or the Lean ecosystem. Those ideas will be built as we need them.

The central promise of the book is this:

Every Lean feature should become visible before it becomes automatic.

Lean can feel mysterious when one only sees code and error messages. This book therefore treats visualization as part of learning, not as decoration. We will draw proof states, term trees, dependency graphs, simplification flows, instance-search graphs, elaboration diagrams, and recursion call graphs. These pictures will not replace Lean’s formal checking. They will help you see what Lean is doing.

Why formalized mathematics matters

In ordinary mathematics, a proof is accepted when competent readers agree that the argument is correct. This social process is powerful, subtle, and historically successful, but it is not the same as mechanical verification. Human-written proofs often omit routine algebra, type information, domain conditions, or uses of earlier lemmas. Usually this is good style. A proof that says every tiny inference would be unreadable.

A proof assistant changes the division of labor. The human still chooses definitions, invents lemmas, guides the proof, and decides what is mathematically important. The computer checks the formal details.

A simple informal proof might say:

If \(p\) and \(q\), then \(q\) and \(p\).

A Lean proof must make the structure explicit:

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
  intro h
  exact And.intro h.right h.left

Read this slowly.

The theorem says:

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p

This means: for propositions p and q, if we have a proof of p ∧ q, then we can build a proof of q ∧ p.

The proof begins:

by
  intro h

The command intro h says: assume the premise p ∧ q, and call that assumption h.

From h : p ∧ q, Lean knows two projections:

h.left  : p
h.right : q

So the final line constructs a proof of q ∧ p:

exact And.intro h.right h.left

The constructor And.intro builds a proof of a conjunction. Since the goal is q ∧ p, it needs first a proof of q, then a proof of p. Those are exactly h.right and h.left.

Visually:

Given:

  h : p ∧ q

Lean can project:

  h.left  : p
  h.right : q

Goal:

  q ∧ p

Build:

  And.intro h.right h.left
      │        │
      │        └── proof of p
      └─────────── proof of q

This is a tiny example, but it already contains the heart of formalization. A proof is not merely a paragraph. It is an object with a type. Lean checks that the object has the claimed type.

This idea is known as the propositions-as-types principle, also associated with the Curry–Howard correspondence: propositions can be represented as types, and proofs as terms inhabiting those types. Lean’s logical foundation is based on this general perspective, implemented through dependent type theory (de Moura et al., 2015; Avigad et al., 2024).

Lean as three things at once

At first, Lean can be confusing because it is not just one kind of tool. It is useful to see it as three interconnected things.

                 Lean
                  │
     ┌────────────┼────────────┐
     │            │            │
Programming   Proof        Mathematical
language      assistant    library platform

Lean is a programming language. You can define functions and evaluate expressions:

def twice (f : Nat → Nat) (n : Nat) : Nat :=
  f (f n)

#eval twice (fun x => x + 1) 10

The result is:

12

Here Nat is the type of natural numbers, Nat → Nat is the type of functions from natural numbers to natural numbers, and fun x => x + 1 is an anonymous function that adds one.

Lean is also a proof assistant. It helps you construct proofs and checks them:

example : 2 + 3 = 5 := by
  rfl

The tactic rfl proves goals that are true by reflexivity after computation or definitional reduction. In this case, Lean can reduce 2 + 3 to 5, so the equality is accepted.

Lean is also a platform for formalized mathematics. Its library ecosystem, especially Mathlib, contains a large body of formalized mathematics, including algebra, order theory, topology, analysis, category theory, and many supporting structures. Mathlib is designed as a shared library of definitions, theorems, tactics, and conventions for Lean formalization (The mathlib Community, 2020).

These three roles are not separate compartments. They reinforce one another. Lean’s programming language lets us define mathematical objects. Its proof assistant lets us prove theorems about them. Its libraries let us build on previous formal work instead of starting from zero.

What a theorem prover actually checks

A theorem prover does not “understand” mathematics in the way a human researcher does. It checks formal expressions according to precise rules.

A helpful first model is this:

Human writes Lean code
        │
        ▼
Elaborator fills in details
        │
        ▼
Kernel checks core terms
        │
        ▼
Accepted declaration enters environment

The elaborator is the part of Lean that turns user-friendly Lean syntax into more explicit internal expressions. When you write something concise, Lean often infers missing arguments, inserts implicit information, resolves overloaded notation, and creates internal proof obligations.

The kernel is the small trusted part of Lean that checks whether the final elaborated term is valid. A system with a small kernel follows an important design principle: many convenient tools may help produce a proof, but the final proof object must still be checked by a small trusted core. Lean follows this architecture (de Moura et al., 2015; Lean FRO, 2025).

For example, the proof:

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  exact And.intro hp hq

can be pictured as a construction:

hp : p        hq : q
  │             │
  └──────┬──────┘
         ▼
   And.intro hp hq : p ∧ q

Lean accepts the theorem because the constructed proof term has exactly the required type.

This distinction is important throughout the book. Tactics, automation, notation, macros, and library search are powerful, but they do not replace the kernel. They help build terms that the kernel checks.

The first mental shift: from truth to inhabitation

In ordinary propositional logic, we often ask whether a proposition is true or false. In Lean, we often ask whether a type has an inhabitant.

An inhabitant of a type is a term of that type. For example:

#check 3

Lean reports that 3 has type Nat.

So 3 is an inhabitant of Nat.

For propositions, a proof is an inhabitant. If p : Prop, then a term of type p is a proof of p.

example (p : Prop) (hp : p) : p :=
  hp

Here:

p  : Prop
hp : p

The assumption hp is already a proof of p, so the theorem is proved by returning hp.

This is not merely a trick. It is a disciplined way of making proof checking computationally precise. The statement of a theorem is a type. A proof is a term of that type. Lean checks that the term fits.

The second mental shift: definitions matter as much as proofs

When learning mathematics informally, students often focus on theorems. In formalized mathematics, definitions become equally central.

A poor definition can make every later proof difficult. A good definition can make later theorems almost inevitable.

For example, suppose we define a simple predicate on natural numbers:

def IsZero (n : Nat) : Prop :=
  n = 0

This is a definition of a proposition depending on a number. If n is a natural number, then IsZero n is the proposition that n = 0.

Now we can prove:

example : IsZero 0 := by
  rfl

Because IsZero 0 unfolds to 0 = 0, rfl proves it.

Visually:

Goal:
  IsZero 0

Unfold definition:
  0 = 0

Solved by:
  rfl

This example is tiny, but the pattern scales. In large formalization projects, choosing the right definitions is one of the main intellectual tasks. We will repeatedly ask:

• What object should be represented as a type?
• What property should be represented as a predicate?
• What data should be bundled into a structure?
• What should be inferred by type class search?
• What should be stated as a theorem rather than built into a definition?

These questions are part of mathematical design.

The third mental shift: proof is interaction

Lean proof development is interactive. You usually do not write a complete proof perfectly on the first attempt. Instead, you inspect the current goal, apply a tactic or term, observe the new goals, and continue.

The interaction looks like this:

Initial goal
    │
    ▼
Apply tactic
    │
    ▼
New goal state
    │
    ▼
Apply next tactic
    │
    ▼
No goals remaining

For example:

example (p q : Prop) : p ∧ q → q ∧ p := by
  intro h
  constructor
  · exact h.right
  · exact h.left

After intro h, the proof state is conceptually:

Context:
  p q : Prop
  h : p ∧ q

Goal:
  q ∧ p

After constructor, Lean splits the conjunction goal into two goals:

Goal 1:
  q

Goal 2:
  p

Then each goal is solved from h.

Goal 1: q   solved by h.right
Goal 2: p   solved by h.left

This style will become familiar. Tactic proofs are not magic scripts. They are controlled transformations of proof states.

What this book will teach you to see

A central difficulty in learning Lean is that several layers operate at once. The same line of Lean code may involve parsing, name resolution, implicit argument inference, type class synthesis, coercions, simplification, reduction, and kernel checking. Beginners often see only the surface. Experts learn to see the layers.

This book will train that expert vision.

When we later write:

simp

we will not treat it as a spell. We will ask:

What is the goal?
Which simp lemmas are available?
In what direction are they used?
Did any definitions unfold?
Did simplification solve the goal or only transform it?

When Lean finds an instance automatically, we will ask:

What class is being synthesized?
Which instances are candidates?
Which priorities matter?
Is there a diamond?
Is the result stable under imports?

When a recursive definition fails, we will ask:

What recursive calls were found?
Which argument decreases?
Is the decrease structural?
Is a well-founded relation needed?

When a theorem from Mathlib almost fits, we will ask:

Is the mismatch caused by notation?
By coercions?
By implicit arguments?
By universe levels?
By a different representation of the same concept?

These questions are the path from competence to mastery.

A first map of the journey

The book is organized as a long ascent.

The early chapters build the foundations: what Lean is, how to install and use it, how terms and types work, how propositions become types, and how proofs become terms. These chapters are deliberately careful because later fluency depends on early precision.

The middle chapters teach Lean as a language for mathematics: inductive types, recursion, pattern matching, structures, type classes, notation, modules, tactics, simplification, attributes, coercions, quotients, universes, and classical reasoning.

The later chapters teach Lean as a research and engineering environment: reading Mathlib, formalizing discrete mathematics, working with algebraic hierarchies, navigating topology and analysis interfaces, building custom automation, debugging hard failures, organizing large projects, and designing visual demonstrations for Lean features.

The final chapters are case studies. They show how definitions, lemmas, automation, documentation, and project structure grow together in real formalization work.

The journey can be pictured like this:

Programming basics + propositional logic
              │
              ▼
      Terms, types, propositions
              │
              ▼
     Dependent types and equality
              │
              ▼
   Inductive data, recursion, structures
              │
              ▼
      Tactics and automation
              │
              ▼
      Mathlib fluency
              │
              ▼
   Large formalization projects
              │
              ▼
      Expert theorem proving

You should not expect to master every topic on first reading. Lean rewards revisiting. A concept that feels abstract in Chapter 5 may become concrete when you use it in Chapter 15. A confusing error message in Chapter 10 may become obvious after Chapter 30. The book is designed so that ideas return with increasing depth.

How to work through examples

Every Lean example in this book should be treated as executable mathematics. Do not only read the code. Run it. Modify it. Break it. Repair it.

When you see a theorem, try the following routine:

1. Read the statement before reading the proof.
2. Translate the statement into ordinary mathematical language.
3. Identify the assumptions and the goal.
4. Predict what the first proof step should do.
5. Run the code in Lean.
6. Delete one line and observe the error.
7. Restore the line and explain why it works.

For example, with:

example (p q : Prop) (hp : p) (hq : q) : q ∧ p := by
  constructor
  · exact hq
  · exact hp

Ask:

• What are p and q?
• What are hp and hq?
• Why does constructor create two goals?
• Why is hq used before hp?
• What happens if the two final lines are swapped?

If you swap them, Lean will complain because the first goal is q, but hp proves p. This is a useful error. It means Lean is protecting the exact structure of the proof.

What “visual” means in this book

A visualization in this book is not a vague illustration. It is a disciplined diagram of a formal process.

For example, a proof-state timeline shows how tactics transform goals:

Before intro:

  p q : Prop
  ⊢ p ∧ q → q ∧ p

After intro h:

  p q : Prop
  h : p ∧ q
  ⊢ q ∧ p

After constructor:

  Goal 1:
    p q : Prop
    h : p ∧ q
    ⊢ q

  Goal 2:
    p q : Prop
    h : p ∧ q
    ⊢ p

A term tree shows how a term is built from smaller terms:

And.intro h.right h.left
├── h.right : q
└── h.left  : p

A dependency graph shows which declarations depend on which earlier declarations:

IsZero
  │
  ▼
example : IsZero 0

A simplification trace shows how an expression changes:

IsZero 0
   unfolds to
0 = 0
   solved by
rfl

These diagrams are meant to make Lean’s internal activity legible. They are approximations for learning, but they must remain faithful to the formal structure.

The attitude of formalization

Formalized mathematics requires patience, but not passive patience. It requires active precision.

When Lean rejects a proof, it is not saying that you are bad at mathematics. It is saying that a particular term has not yet been shown to have a particular type. That message may be caused by a genuine mathematical gap, a missing lemma, a coercion issue, an ambiguous notation, an unhelpful definition, a failed type class search, or simply a typo.

Expert Lean users are not people who never see errors. They are people who can interpret errors productively.

The healthiest attitude is:

Lean error
   │
   ▼
Information about a mismatch
   │
   ▼
Question about the formal structure
   │
   ▼
Improved definition, statement, or proof

This book will teach that loop repeatedly.

Beginning

We now begin with the first orientation: what Lean is, how formalization changes the practice of mathematics, and why the small kernel, elaborator, theorem statements, proof terms, tactics, and libraries fit together into one coherent system.

The first chapter will not assume that you already know type theory or proof assistant architecture. It will build the map from first principles.

Keep one idea in mind as you start:

Lean is not only a language for writing proofs. It is a language for making mathematical meaning checkable.

References

Avigad, Jeremy, Leonardo de Moura, Soonho Kong, and Sebastian Ullrich. 2024. Theorem Proving in Lean 4. https://lean-lang.org/theorem_proving_in_lean4/

de Moura, Leonardo, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. “The Lean Theorem Prover (System Description).” In Automated Deduction — CADE-25, Lecture Notes in Computer Science 9195, 378–388. Springer. https://doi.org/10.1007/978-3-319-21401-6_26

Lean FRO. 2025. The Lean Language Reference. https://lean-lang.org/doc/reference/latest/

The mathlib Community. 2020. “The Lean Mathematical Library.” In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 367–381. ACM. https://arxiv.org/abs/1910.09336