Lecture 4 — Introduction to Lean

Abstract

From paper to kernel. We meet Lean 4: the difference between term mode and tactic mode, between propositions and data, the natural numbers and induction, and the handful of tactics that get you to a first honest end-to-end proof. We anchor the practice in the Natural Number Game and Heather Macbeth’s Mechanics of Proof.

Learning objectives

By the end of this lecture you can:

• Read the same theorem in term mode (a bare \(\lam\)-term) and tactic mode (a by script), and explain why both elaborate to one kernel-checked term — the de Bruijn criterion.

• Distinguish Prop (proof-irrelevant propositions) from Type/data and use the Curry–Howard dictionary — \(\To\) a function, \(\land\) a pair, \(\exists\) a dependent pair — with intro, exact, apply, constructor, and obtain/rcases.

• Prove statements about the naturals by structural induction, and explain why \(n+0=n\) holds by rfl but \(0+n=n\) needs induction.

• Drive equational reasoning with rfl, rw (including the reverse rw [← h]) and simp, controlling direction and order.

• Choose the right automation — decide, omega, ring, linarith — and state each one’s scope and failure mode.

• Set up a real Lean 4 + Mathlib project (elan, lake, lake exe cache get, a pinned lean-toolchain) and inspect proofs with #check, #eval, #print axioms.

• Complete one honest end-to-end proof (Gauss’s sum by induction) and one library-driven corollary, then continue independently in NNG4 and Macbeth.

Why this matters

Three lectures of theory now pay off. In Lecture 1 we met the judgment \(\Gamma \proves t : A\); in Lecture 2 we computed with pure \(\lam\)-terms; in Lecture 3 we read the connectives as type formers. Lean 4 is that story made executable. It is a dependently-typed \(\lam\)-calculus in which a proposition is a type and a proof is a term inhabiting it. Nothing new is asked of you conceptually — but now a machine checks every step.

Why should a mathematician trust a machine? Because of a deliberate architectural choice: only a small type-checking kernel must be correct. A proof, however it was produced, is ultimately a term; the kernel verifies that this term has the claimed type. The elaborator, the tactic framework, the pretty-printer — tens of thousands of lines — may all contain bugs without endangering soundness, as long as the term they emit type-checks. This is the de Bruijn criterion, and it is why “the computer says the proof is correct” means something precise. It is also the foundation for the research formalization we build toward in Lecture 6.

The second reason is Mathlib: a single, coherent library holding on the order of \(283{,}000\) theorems and \(135{,}000\) definitions (2026). Formalizing modern mathematics is feasible precisely because you rarely start from nothing — you cite a lemma. Learning to search for the right name is as much a skill as learning to prove.

Two modes, one term: term mode, tactic mode, and the kernel

In Lean every proof is a term. You can write that term two ways.

Term mode — write the inhabitant directly. Modus ponens is literally function application:

theorem modus_ponens {P Q : Prop} : (P → Q) → P → Q :=
  fun f p => f p

Tactic mode — a by block whose tactics are a metaprogram that builds the term for you:

theorem modus_ponens' {P Q : Prop} : (P → Q) → P → Q := by
  intro f p
  exact f p

These are not two kinds of proof. by is a term-builder; when it finishes, Lean hands the kernel a \(\lam\)-term, exactly as term mode does. You can always see it: after a tactic proof, #print modus_ponens' reveals fun f p => f p. The universe bookkeeping behind this is small: every type lives in some Sort u, with Prop = Sort 0 for proof-irrelevant propositions and Type = Type 0 = Sort 1 for data.

So does every proof “fully expand” into one giant λ-term? No — three precisions

Names stay names. The elaborated term references the lemmas it uses as constants — #print on this course’s add_comm' shows Nat.recAux, Eq.mpr, and the names zero_add'/succ_add', not their inlined proofs. Proofs form a shared DAG; the kernel unfolds a definition lazily only when a definitional-equality check demands it, and never β-normalizes your proof. This sharing is what makes a 283 000-theorem library feasible. (Our lab’s let expands eagerly at definition time — the miniature version; Lean keeps a persistent name table instead.)

Some terms are small because the kernel computes. theorem four : 2 + 2 = 4 := by decide elaborates to just of_decide_eq_true (id (Eq.refl true)) — the work happens when the kernel evaluates decide (2 + 2 = 4) to true during checking. Term size and checking effort are decoupled in both directions: simp builds long explicit Eq.mpr chains, decide builds two nodes.

The compiler erases proofs entirely. Elaborated terms have two consumers: the kernel certifies everything (including all of Prop), while the code generator erases Prop as computationally irrelevant — a proof is checked once, stored as a compressed expression in the .olean, and never becomes runtime code. Even sorry is a term (sorryAx …), which is exactly why #print axioms can audit for it.

Run it

Experience “tactics build a term” before Lean is even installed — each direction is one lab command:

• prove (P -> Q) -> P -> Q — an interactive proof builder: type intro f, intro p, apply f, assumption, then qed.

• ch term \f. \p. f p — infers the principal type of the hand-written λ-term.

qed prints the extracted term λf p. f p with the type it proves: the tactics were a program that built the term, and qed is your #print — the de Bruijn criterion on one screen.

Worked example 1 (symmetry of conjunction, both ways). Conjunction is a structure with two fields, so a proof of \(P \land Q\) is a pair, and swapping is trivial:

-- term mode: destructure the pair, rebuild it swapped
theorem and_comm_term {P Q : Prop} : P ∧ Q → Q ∧ P :=
  fun ⟨hp, hq⟩ => ⟨hq, hp⟩

-- tactic mode: the SAME term, built step by step
theorem and_comm_tac {P Q : Prop} (h : P ∧ Q) : Q ∧ P := by
  obtain ⟨hp, hq⟩ := h   -- split the hypothesis into hp : P, hq : Q
  constructor            -- goal Q ∧ P becomes two goals: Q, then P
  · exact hq
  · exact hp

Run #print and_comm_tac and you get fun h => ⟨h.2, h.1⟩ — the anonymous constructor and projections of the same structure. Term mode and tactic mode differ only in how much of the term you write.

Run it

Project the sources on screen and run them through the lab: lean and_comm, lean term_proofs, lean imp_comp. The same tautologies appear in all four provers — compare artifacts/lean, artifacts/agda, artifacts/rocq and artifacts/mizar.

Propositions vs data: Prop, proof irrelevance, and the Curry–Howard dictionary

Here is the distinction that trips up every mathematician. A proposition P : Prop is proof-irrelevant: any two proofs of P are equal, so a proof carries no information beyond “this holds.” Data n : Nat is not: 2 and 3 are different. Consequently you may not, in general, pattern-match on a proof to extract data (the large-elimination restriction) — a proof of \(\exists n,\ \dots\) does not hand you a computable witness in Type.

Tip

Why can’t I extract the witness? Because proof irrelevance forces functions out of proofs to be constant. Suppose you could pattern-match h : ∃ n, 2 ∣ n and return the witness. The proofs ⟨2, _⟩ and ⟨4, _⟩ inhabit the same proposition, so they are equal — yet your extractor would send equal inputs to the unequal outputs 2 and 4. Contradiction; hence the restriction. When you genuinely need the witness as data, use the Type-valued siblings — the subtype {n // 2 ∣ n} or a sigma type Σ n, … — whose elements really are pairs you may take apart.

Everything else is the dictionary you already know from Lecture 3, now as concrete datatypes:

Logic	Lean type	Introduce	Eliminate
\(P \To Q\)	function P → Q	fun h => … / intro	apply it
\(P \land Q\)	structure And P Q	⟨_, _⟩ / constructor	.left, .right / obtain
\(P \lor Q\)	sum Or P Q	Or.inl, Or.inr / left,right	rcases/cases
\(\exists x,\ p\,x\)	dependent pair Exists p	⟨w, hw⟩	obtain ⟨w, hw⟩ := h
\(P \Leftrightarrow Q\)	structure Iff P Q	⟨mp, mpr⟩	.mp, .mpr
\(\forall x,\ p\,x\)	dependent function (x : α) → p x	fun x => … / intro	apply it

The punchline students remember: \(\exists\) is not a mystical quantifier, it is a pair type. Its constructor is \(\langle \text{witness}, \text{proof} \rangle\); its eliminator is destructuring.

Worked example 2 (an existential is a pair).

-- the proof IS the pair (witness 2, a proof that 2^2 = 4)
theorem exists_sq_four : ∃ n : Nat, n ^ 2 = 4 := ⟨2, rfl⟩

Why does rfl prove \(2^2 = 4\)? Because on Nat the expression \(2^2\) computes to \(4\); the two sides share a normal form, so they are definitionally equal. The same phenomenon explains a slogan you will meet constantly: 2 ∣ n is by definition ∃ c, n = 2 * c. The two are the same proposition — no lemma is needed to pass between them, only destructuring:

theorem two_dvd_iff (n : Nat) : 2 ∣ n ↔ ∃ c, n = 2 * c :=
  ⟨fun h => h, fun h => h⟩   -- both directions are the identity: same type

The natural numbers and induction

Nat is an inductive type — Peano’s axioms as data constructors, exactly the zero/succ of Lecture 2, now with a real recursor:

inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

Addition is defined by structural recursion on its second argument:

\[ m + 0 = m, \qquad m + (n+1) = (m + n) + 1. \]

This asymmetry is the single most instructive surprise of the day. Because the recursion consumes the right operand, \(m + 0 = m\) is the defining equation — it holds by rfl. But \(0 + n = n\) is not a defining equation (the recursion never looks at a left zero), so it must be proved, by induction on \(n\).

Worked example 3 (rebuilding addition, as in NNG4). On a private copy of the naturals we reconstruct commutativity from the two defining equations alone:

inductive N where
  | zero : N
  | succ : N → N

namespace N

def add (m : N) : N → N
  | .zero   => m                 -- add_zero: m + 0     = m
  | .succ n => .succ (add m n)   -- add_succ: m + (n+1) = (m + n) + 1

@[simp] theorem add_zero (m : N)   : add m .zero = m := rfl
@[simp] theorem add_succ (m n : N) : add m (.succ n) = .succ (add m n) := rfl

theorem zero_add (n : N) : add .zero n = n := by
  induction n with
  | zero      => rfl                    -- add .zero .zero = .zero  by rfl
  | succ k ih => rw [add_succ, ih]      -- succ (add .zero k) → succ k

theorem succ_add (m n : N) : add (.succ m) n = .succ (add m n) := by
  induction n with
  | zero      => rfl
  | succ k ih => rw [add_succ, ih, add_succ]

theorem add_comm (m n : N) : add m n = add n m := by
  induction n with
  | zero      => rw [add_zero, zero_add]
  | succ k ih => rw [add_succ, succ_add, ih]

Read add_comm slowly, because it is the whole method in four lines. induction n splits into the base case (\(n = 0\)), closed by rewriting both sides to \(m\), and the successor case, which assumes the induction hypothesis ih : add m k = add k m and rewrites the goal \(\text{add } m\,(k{+}1) = \text{add }(k{+}1)\,m\) down to a syntactic identity using, in order, add_succ, succ_add, and ih. This is precisely the milestone the Natural Number Game’s Addition World hands you a star for.

Run it

Play the Natural Number Game through the Tutorial and Addition worlds — no installation, it runs in the browser and culminates in exactly this add_comm. Then see the offline trace with lean add_comm. The Agda twin +-comm and the Rocq twin add_comm (via induction n + rewrite) live in the four-prover artifacts.

Rewriting: rfl, rw, simp

Equational reasoning is the everyday mechanics, and its three tools have sharply different jobs.

• rfl closes a = a when both sides are definitionally equal — reduce to a common normal form. It proves \(m + 0 = m\) and \(2^2 = 4\); it does not prove \(0 + n = n\).

• rw [h] rewrites the goal left-to-right by the equation h, replacing occurrences of its LHS with its RHS. It fails if the LHS does not appear syntactically, and can raise motive is not type correct in dependent situations. Use rw [← h] for the reverse direction, and chain rw [h₁, h₂, …] to apply several in order. After a rw that makes both sides identical, the goal is closed automatically.

• simp repeatedly rewrites with the whole @[simp] lemma set (plus arithmetic/definitional simplification) until nothing applies. It is non-directional and powerful, but opaque — reach for a targeted rw when you know the exact step, and simp only [lemmas] when you want a controlled subset.

A pure rw chain — no induction — illustrates the discipline; here ← is essential:

example (a b : ℝ) (h1 : a^2 = b^2 + 4) (h2 : a + b = 2) : (a - b) * 2 = 4 := by
  have hprod : (a - b) * (a + b) = 4 := by
    have : a^2 - b^2 = 4 := by linarith
    calc (a - b) * (a + b) = a^2 - b^2 := by ring
      _ = 4 := this
  rw [← h2]        -- turn the goal's `2` back into `a + b`, matching hprod
  exact hprod

A first honest end-to-end proof — and a library-driven corollary

Two mental models coexist in formal mathematics: I can build a proof from primitives, and the right move is usually to find the lemma. You need both.

Worked example 4 (Gauss’s sum, built by induction). The schoolchild identity, kernel-checked:

\[ 2\sum_{k=0}^{n} k = n(n+1). \]

import Mathlib

theorem gauss (n : Nat) : 2 * (∑ k ∈ Finset.range (n + 1), k) = n * (n + 1) := by
  induction n with
  | zero      => simp                                    -- both sides are 0
  | succ n ih => rw [Finset.sum_range_succ, Nat.mul_add, ih]; ring

The base case is simp (it knows the empty-then-single-term sum reduces and \(0 = 0\cdot 1\)). The step peels off the last summand with Finset.sum_range_succ, distributes with Nat.mul_add, substitutes the induction hypothesis ih, and lets ring clear the polynomial dust. That is a complete, sorry-free proof of a genuine theorem.

Worked example 5 (the library-driven idiom). Euclid’s theorem — infinitely many primes — is already in Mathlib as Nat.exists_infinite_primes. The everyday move is to cite it and align types:

theorem prime_above (N : Nat) : ∃ p, N < p ∧ p.Prime := by
  obtain ⟨p, hN, hp⟩ := Nat.exists_infinite_primes (N + 1)  -- gives N + 1 ≤ p
  exact ⟨p, by omega, hp⟩                                    -- omega: N + 1 ≤ p ⟹ N < p

You did not reprove Euclid; you found the name, destructured its output, and let omega promote \(N + 1 \le p\) to \(N < p\). Searching (exact?, apply?, Loogle, LeanSearch) is a core skill, not cheating — the same idiom makes Irrational (Real.sqrt 2) a one-liner on top of Nat.Prime.irrational_sqrt, developed further in Lecture 5.

Run it

Walk the guided tutorial that chains narrative → live proof-term inspection → a checkpoint quiz: tutorial 1 (the Gauss bundle), then ch explore --live to see the finished proof as a term tree, and kb mathlib for the lemma-search cheatsheet.

Arithmetic automation: decide, omega, and a peek at ring/linarith

Beginners either fall in love with automation or get burned by it. The cure is knowing each tactic’s scope.

Tactic	Discharges	Fails / out of scope when…
decide	a decidable proposition, by evaluating its Decidable instance to isTrue	the goal is not decidable, or is decidable but too large to compute
omega	linear integer/natural arithmetic — equalities, inequalities, ∣ by literals (Presburger)	any product of variables, e.g. x * y
ring / ring_nf	identities in a commutative (semi)ring	(in)equalities, or non-ring goals
linarith / nlinarith	linear (and, heuristically, nonlinear) inequalities from hypotheses	needs the right hints; not a normalizer

Two contrasts make the point. First, ⟨2, rfl⟩ and by refine ⟨2, ?_⟩; decide both prove \(\exists n,\ n^2 = 4\) — one by definitional computation, one by running a decision procedure. Second, the misconception “just try omega” wastes real time: omega will not touch \(x \cdot y\), and reaching for it on a nonlinear goal simply fails. Match the tactic to the shape of the goal.

Run it

Every row of this table is a card in the lab’s Lean tactic encyclopedia — summary, effect on the goal, when to reach for it, and a worked example: ch tactic decide · ch tactic omega · ch tactic ring · ch tactic linarith. Exercise 7 (automation scope) is easiest after reading the omega and ring cards side by side.

Tooling: elan, lake, Mathlib, and #check/#eval

The unglamorous but decisive half of “introduction to Lean.”

# one-time: install the toolchain manager, then Lean + lake come with it
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

# a fresh Mathlib-backed project
lake +leanprover-community/mathlib4:lean-toolchain new my_project math
cd my_project
lake exe cache get          # download prebuilt Mathlib .olean files — do NOT skip this
lake build

Three points a mathematician must internalize:

• elan pins the exact compiler per project via a lean-toolchain file, e.g. leanprover/lean4:v4.28.0-rc1. The current stable line is Lean 4.32.0 (2026-07); the author’s own demo repo pins v4.28.0-rc1 and the EML formalization targets Lean v4.28 — deliberate version skew is normal, and pinning both toolchain and Mathlib is what makes a build reproducible.

• lake exe cache get downloads prebuilt .olean artifacts. Skip it and you recompile ~300k theorems from source — hours on a laptop.

• Inspection is instant. #check Nat.add_comm reports ∀ (n m : ℕ), n + m = m + n; #eval 2 ^ 10 prints 1024; and — the trust audit you should always run — #print axioms gauss lists exactly the axioms a proof depends on, confirming there is no hidden sorry.

Common pitfalls

• “Term mode and tactic mode are different kinds of proof.” They are not. A by block is a metaprogram that builds a \(\lam\)-term; the kernel checks that term. Any tactic proof can be #printed as a term.

• “rfl closes every equality.” It closes only definitional ones. add_zero : m + 0 = m is rfl; zero_add : 0 + n = n is not, because Nat.add recurses on its second argument. This asymmetry surprises everyone.

• Misusing rw. It rewrites strictly left-to-right and fails if the LHS is not present syntactically (or throws motive is not type correct). Forgetting rw [← h] for the reverse direction, or reaching for simp where a targeted rw is needed (or vice versa), is the usual beginner friction.

• Treating Prop like data. Propositions are proof-irrelevant; you cannot pattern-match on a proof to extract computational data (large-elimination restriction).

• Over-trusting automation. decide needs a Decidable instance and can hang; omega is linear only and will not touch x * y. “Just try omega/decide” is a real time sink.

• Assuming NNG4 transfers verbatim. The game curates a subset and lightly renames things; production Lean uses induction n with | … => …, full Mathlib names, and omega/ring/simp the game may hide.

• Underestimating install friction. Skipping lake exe cache get, or a lean-toolchain that does not match your Mathlib version, breaks reproducibility.

• Fighting the surface syntax. Lean is indentation- and Unicode-sensitive: enter \(\forall\,\exists\,\to\,\land\,\leftrightarrow\,\N\) via \forall, \exists, \to, \and, \iff, \N. And {P Q : Prop} (implicit) vs (h : P ∧ Q) (explicit) changes how you call a lemma.

Exercises

1. (Composition, both modes.) Prove (P → Q) → (Q → R) → P → R in term mode (fun f g p => g (f p)) and in tactic mode (by intro f g p; exact g (f p)). Then #print both and confirm they are the same term.

2. (Squares.) Prove ∃ n : Nat, n ^ 2 = 4 first as the pair ⟨2, rfl⟩, then as by refine ⟨2, ?_⟩; decide. Explain in one sentence why rfl already works.

3. (NNG4, pen-and-paper first.) Before touching Lean, write out, by hand, the two-case induction for zero_add and add_comm on N. Then clear NNG4’s Addition World and check your cases matched.

4. (Rewrite discipline.) On the private naturals N, prove add_right_comm (a b c : N) : add (add a b) c = add (add a c) b using only rw with add_assoc and add_comm — no induction. (Hint: you will need at least one rw [← …].)

5. (Gauss.) Reproduce Worked Example 4 in a Mathlib project and run #print axioms gauss. Confirm the output contains no sorryAx.

6. (Library hunt — medium.) Prove ∃ p, 100 < p ∧ p.Prime by finding the Mathlib lemma with exact? and finishing with omega. Name the lemma you used.

7. (Automation scope — medium.) Exhibit one goal that omega closes and ring cannot, and one that ring closes and omega cannot. State why in each case.

8. (Cross-prover — hard.) Prove commutativity of addition on your own inductive naturals in two systems: Lean (induction + rw) and Agda (+-comm by pattern-matching induction), starting from the four-prover artifacts. Contrast how each system presents the induction hypothesis. (Optional: add the Rocq version with induction + lia.)

References

• Theorem Proving in Lean 4 — Avigad, de Moura, Kong, Ullrich: the canonical free introduction to term/tactic mode, Prop vs Type, and inductive types. The best reading to assign after this lecture.

• Mathematics in Lean — Avigad, Massot: the hands-on Mathlib tutorial (rw/simp/ring/linarith, Nat, sets).

• Natural Number Game 4 (NNG4) — the zero-install browser game that reconstructs Nat from Peano and drills exactly this lecture’s induction+rw up to add_comm.

• The Mechanics of Proof — Heather Macbeth: every proof in both prose and Lean, at first-year level; source of the calc/have/linarith style.

• Lean install guide (elan + lake) and the Lean release notes — current tooling and the version anchor.

• Mathlib4 statistics — the live theorem and definition counts behind “citing a lemma is the normal mode.”

• The Lean 4 Theorem Prover and Programming Language — de Moura, Ullrich: the system’s design and the small-trusted-kernel / de Bruijn criterion.

• The course’s own four-prover artifacts and the Lean sources.

Note

This chapter is the write-up of Part IV of the falenty-2026 course; NNG4 and Macbeth are the intended self-study ramps out of it, and the EML formalization of Lecture 6 is where it leads.