Lean 4 Essentials for Mathematicians

Why This Matters

A mathematician approaching Lean 4 for the first time encounters a programming language being used as a proof assistant. Most introductory material is written for programmers learning theorem proving; the inverse audience needs a different entry. This page covers the minimum set of Lean 4 concepts you need to read a typical Mathlib proof or write a short one, with no prior programming background.

Lean 4 is a dependently typed programming language. Every object has a type. Types themselves are objects of a higher type. Propositions are types whose inhabitants are proofs. Writing a proof is constructing an inhabitant of the type that represents the proposition. The kernel is the small, audited piece of software that checks the constructed term against the proposition. That is the entire system.

The Five Things to Know

1. Types and propositions. Every term x has a type, written x : T. Some types are familiar: Nat, Int, Real, List Nat, Set Real. Some types are propositions: 2 + 2 = 4, ∀ n : Nat, n + 0 = n, ∃ x : Real, x^2 = 2. The type universe Prop collects all propositions; Type collects all data types. A proof of a proposition P : Prop is a term h : P. Constructing such a term is what it means to prove P.

2. Dependent types. A type can depend on a value. Vector Nat n is a list of Nat of length exactly n. The type changes when n changes. This is why theorems with universal quantifiers translate cleanly: ∀ n : Nat, P n is the type of functions that, given n, return a proof of P n. Dependent types are what make Lean a theorem prover and not just a programming language.

3. The kernel. Lean's trusted base is a small program (a few thousand lines) that checks one thing: given a candidate term t and a claimed type T, does t : T hold? Tactics, automation, simp lemmas, decision procedures: none of this is trusted. They emit terms; the kernel checks the terms. The trust boundary is sharp: if the kernel accepts a proof of False, the system is broken. As of Lean 4 with the standard axioms (propext, Classical.choice, Quot.sound), no such proof is known.

4. Tactic mode versus term mode. A theorem can be proved by writing the term directly:

theorem add_zero (n : Nat) : n + 0 = n := rfl

Or by invoking tactics:

theorem add_zero (n : Nat) : n + 0 = n := by rfl

Tactics are programs that build the term. by opens tactic mode; everything until the proof closes is tactic syntax. Most modern Mathlib proofs are tactic-mode. See tactic vs term mode for the practical rule on when each is appropriate.

5. The standard tactics. Five tactics cover roughly 80 percent of proof closings:

• rfl: proves a = a (and anything that reduces to a = a by definitional unfolding).
• simp: rewrites using a curated set of simplification lemmas marked @[simp]. The default closer for algebraic manipulation.
• omega: decides linear arithmetic over Nat and Int. Will close any goal of the form $2 n \leq n + 5 \implies n \leq 5$.
• aesop: combines simp with case splitting and lemma search. Catches a lot of "obvious" goals.
• grind: heuristic Knuth-Bendix-style closer added in Lean 4.10+. Sometimes catches goals the others miss.

The discipline is to try rfl first (cheapest), then simp, then omega or aesop, then grind, and only fall back to manual term construction when none close the goal.

The Trust Story

A Lean proof is "kernel-checked" when the kernel has verified the term constructed by the user (possibly through tactics). Three axioms are admitted as primitive: propositional extensionality, classical choice, and quotient soundness. Any proof that does not use these axioms is constructive; #print axioms my_theorem lists which axioms a specific proof depends on. The FormalSLT project (TheoremPath's Lean dashboard) requires every shipped theorem to print exactly the three standard axioms: no sorryAx, no user-added axioms.

The classical choice axiom is what lets you use the law of excluded middle, decidability of arbitrary propositions, and the standard $\epsilon$-$\delta$ definitions of limits. A proof that avoids Classical.choice is provably valid in intuitionistic logic; the kernel reports this distinction automatically.

Worked Example: add_zero in Three Styles

The theorem "for every natural number $n$, $n + 0 = n$" can be stated and proved in Lean three ways:

Style 1: definitional reduction. The definition of Nat.add makes n + 0 reduce to n by computation. So rfl closes the goal:

theorem add_zero (n : Nat) : n + 0 = n := rfl

Style 2: full term. Spelling out the proof term explicitly:

theorem add_zero (n : Nat) : n + 0 = n :=
  Eq.refl n

Identical in effect; useful when you want to thread the proof into a larger term.

Style 3: tactic mode. When the proof is more complex, switch to tactics:

theorem add_zero (n : Nat) : n + 0 = n := by
  rfl

Trivial here, but the same by ... rfl structure scales to multi-step proofs.

Worked Example: A Multi-Step Proof

Prove that for $n : \mathbb{N}$, if $n \leq 5$ then $n^2 \leq 25$:

theorem sq_le_25 (n : Nat) (h : n ≤ 5) : n^2 ≤ 25 := by
  have h1 : n * n ≤ 5 * 5 := Nat.mul_le_mul h h
  -- h1 : n * n ≤ 25
  simpa using h1

The proof: first establish n * n ≤ 5 * 5 by multiplying both inequalities, then close with simpa which normalizes n^2 to n * n and 5 * 5 to 25. The simpa using h1 pattern means "apply simp to h1 and the goal, then close by hypothesis."

In paper math this is a one-line argument. In Lean it is two lines. The overhead is the bookkeeping that the kernel demands.

Common Misconceptions

Exercise

Problem. State and prove in Lean 4 that for every natural number $n$, $0 \leq n^2$. Find a one-line tactic proof.

Hint. Use Nat.zero_le (or equivalently, observe that the result type is Prop and the goal is the universal statement applied to an arbitrary n).

Solution.

theorem nat_sq_nonneg (n : Nat) : 0 ≤ n^2 := Nat.zero_le _

The _ lets Lean infer n^2 as the second argument. Nat.zero_le has type ∀ k : Nat, 0 ≤ k (every natural is at least zero), and the kernel checks that the application makes sense. An alternative tactic-mode proof is by positivity once Mathlib is imported.

Implementation Note

To install Lean 4 locally:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
elan toolchain install leanprover/lean4:v4.30.0

Or use the VS Code "Lean 4" extension, which installs everything on first run.

To start a new project that uses Mathlib:

lake new myproject math
cd myproject
lake update
lake build

The first lake build downloads Mathlib (~3 GB) and runs in roughly 20-40 minutes on an M2 laptop. Subsequent builds use the cached object files.

For day-to-day editing, the VS Code extension shows the proof state in the right panel: at every cursor position inside a proof, Lean displays the current goals. This live feedback is what makes tactic-mode proofs ergonomic.

Connection to TheoremPath

TheoremPath maintains the FormalSLT manifest which lists every theorem on the site that has a corresponding kernel-checked Lean proof. The audit methodology and axiom-checking policy live at /methodology and /evidence. The current Mathlib pin is v4.30.0-rc2 with commit hash recorded in data/verification/lean-manifest.json.

A page-by-page example of "paper statement to Lean theorem" is the Hoeffding finite-sum bound. The next page, a worked Lean proof tour, walks through that file annotated line by line.