First steps in Lean

In 1998 Thomas Hales announced a proof of the Kepler conjecture: no way of stacking equal spheres fills space more densely than the familiar pyramid of oranges on a market stall. The proof combined hundreds of pages of argument with enormous computer calculations. After years of work, the referees reported that they were "99% certain" it was correct, but could not check every detail. So Hales started a new project, Flyspeck: to write the entire proof in a language so precise that a computer program could check every single step. It took a team of mathematicians in several countries more than a decade; the check was completed in 2014.

Programs that check proofs are called proof assistants. In 2020 the mathematician Peter Scholze challenged the community to check a difficult new theorem of his and Dustin Clausen's in the proof assistant Lean; a team led by Johan Commelin finished in 2022, and Scholze wrote that the project had clarified parts of the argument for him. Today Lean's community library, Mathlib, contains well over a hundred thousand theorems, from school algebra to research mathematics, every one of them machine-checked.

In this lesson you will write your first Lean proofs. You have seen Lean code throughout the Lumenary; now you will learn to read it, to write it — and to judge precisely what a green checkmark means.

When you write a proof for a person, you can say "clearly" and skip a step. A proof assistant cannot be persuaded that way. It keeps track of two things:

• the goal: what remains to be proved, and
• the hypotheses: what you are allowed to use.

Each step you write changes the goal, and Lean checks that the step is legal. When no goals remain, the proof is complete. If a step is wrong — or missing — Lean refuses and tells you which goal is still open.

The connectives of logic each have a meaning in this language, closely matching the truth tables of propositional logic:

The simplest proofs are computations. Lean evaluates both sides of 2 + 2 = 4, finds the same number, and accepts rfl ("reflexivity: a thing equals itself"):

/-- `2 + 2 = 4`. The proof `rfl` ("reflexivity") asks Lean to compute both sides; they are the
same natural number, so the proof is accepted. -/
theorem two_add_two : 2 + 2 = 4 := rfl

Next, logic. Here is "if $p$ and $q$, then $q$ and $p$", written as a term: a function that takes the pair of proofs ⟨hp, hq⟩ and returns the swapped pair.

/-- If `p` and `q` are both true, then `q` and `p` are both true. As a **term**: a proof of
`p ∧ q → q ∧ p` is a function that takes a proof of `p ∧ q` — a pair `⟨hp, hq⟩` — and
returns a proof of `q ∧ p`, the pair `⟨hq, hp⟩`. -/
theorem and_swap (p q : Prop) : p ∧ q → q ∧ p :=
  fun ⟨hp, hq⟩ => ⟨hq, hp⟩

The same theorem with tactics. Read it alongside the goal state, which Lean displays after each line. After intro h and obtain ⟨hp, hq⟩ := h the state is

p q : Prop
hp : p
hq : q
⊢ q ∧ p

— the hypotheses above the line, the goal after the turnstile ⊢. Then constructor splits the goal into ⊢ q and ⊢ p, and exact hq, exact hp close them.

/-- The same theorem proved with **tactics**, commands that build the proof step by step.
`intro` assumes the hypothesis, `obtain` splits the pair, `constructor` splits the goal
`q ∧ p` into two goals, and `exact` closes each one. -/
theorem and_swap_tactics (p q : Prop) : p ∧ q → q ∧ p := by
  intro h
  obtain ⟨hp, hq⟩ := h
  constructor
  · exact hq
  · exact hp

Implication is a function, so modus ponens — from $p \to q$ and $p$ conclude $q$ — is function application, and chaining implications is composing functions:

/-- **Modus ponens**: from `p → q` and `p`, conclude `q`. A proof of `p → q` *is* a function
from proofs of `p` to proofs of `q`, so we just apply it to `hp`. -/
theorem modus_ponens (p q : Prop) (hpq : p → q) (hp : p) : q :=
  hpq hp

/-- Implications chain: from `p → q` and `q → r`, conclude `p → r`. The proof is the
composite of the two functions. -/
theorem imp_trans (p q r : Prop) (hpq : p → q) (hqr : q → r) : p → r :=
  fun hp => hqr (hpq hp)

An "or" is proved by cases, and the contrapositive of proof techniques is a one-line function once you remember that ¬q means q → False:

/-- `p ∨ q → q ∨ p`, by **cases**: a proof of `p ∨ q` is either a proof of `p` (`inl`) or a
proof of `q` (`inr`), and we handle each case. -/
theorem or_swap (p q : Prop) : p ∨ q → q ∨ p := by
  intro h
  cases h with
  | inl hp => exact Or.inr hp
  | inr hq => exact Or.inl hq

/-- The **contrapositive**: from `p → q`, conclude `¬q → ¬p`. In Lean `¬q` means `q → False`,
so given `hnq : ¬q` and `hp : p` we produce `False` as `hnq (hpq hp)`. -/
theorem contrapositive (p q : Prop) (hpq : p → q) : ¬q → ¬p :=
  fun hnq hp => hnq (hpq hp)

¬¬p → p is true in every row of its truth table, yet it does not follow from the rules we have used. Lean proves it with a classical principle — proof by contradiction — and the axiom list says so honestly:

/-- **Double negation elimination**, `¬¬p → p`, is a truth-table tautology, but it cannot be
proved from the constructive rules used above. Lean proves it with the classical principle
`Classical.byContradiction` (which rests on the axiom of choice), and `#print axioms` reports
this: compare its axiom list with that of `contrapositive`. -/
theorem double_negation (p : Prop) (h : ¬¬p) : p :=
  Classical.byContradiction h

A truth table checks a propositional statement by trying every row; Lean proves it by building a term. Check that both formulas below are tautologies. Then notice the difference the axiom lists revealed: the first has a constructive proof, the second needs classical logic, even though their truth tables look equally innocent.

Equations are tools: if you know h : a = b, then rw [h] replaces a by b in the goal. Here two rewrites turn a = c into c = c, which rw closes automatically:

/-- **Rewriting** with equations: `rw [h₁]` replaces `a` by `b` in the goal `a = c`, giving
`b = c`; `rw [h₂]` turns it into `c = c`, which `rw` closes automatically. -/
theorem rw_chain (a b c : ℕ) (h₁ : a = b) (h₂ : b = c) : a = c := by
  rw [h₁, h₂]

You can rewrite with theorems from the library too. Nat.add_comm a b is the equation a + b = b + a:

/-- Rewriting with **library lemmas**: `Nat.add_comm a b : a + b = b + a` and
`Nat.mul_comm`. After both rewrites the two sides are identical. -/
theorem rw_library (a b : ℕ) : (a + b) * 2 = 2 * (b + a) := by
  rw [Nat.add_comm a b, Nat.mul_comm]

simp is a more powerful automatic rewriter: it uses hundreds of simplification lemmas such as $x + 0 = x$, $x \cdot 1 = x$ and $x \cdot 0 = 0$, repeatedly, until nothing more changes.

/-- `simp` rewrites with a large collection of simplification lemmas (`x + 0 = x`,
`x * 1 = x`, `x * 0 = 0`, …) until nothing more applies. -/
theorem simp_example (a b : ℕ) : (a + 0) * 1 + b * 0 = a := by
  simp

Lean's natural numbers are built from two constructors: 0, and the successor n + 1 of any natural number $n$. Addition is defined by recursion on the second argument:

The first rule is literally the statement $n + 0 = n$, so Lean accepts it by rfl for every $n$:

/-- `n + 0 = n` holds **by definition**: Lean defines addition by recursion on the second
argument, with `n + 0 = n` as the first rule. So `rfl` works, for every `n`. -/
theorem add_zero_rfl (n : ℕ) : n + 0 = n := rfl

But $0 + n = n$ is different. With $n$ an unknown number, neither rule applies to $0 + n$ — the second argument $n$ is neither $0$ nor visibly of the form $k + 1$ — so the computation is stuck and rfl fails. We need a proof by induction.

In Lean, each line of the human proof becomes one step:

/-- `0 + n = n` is **not** true by definition (the recursion is on the second argument, here
the unknown `n`), so `rfl` fails and we prove it by **induction** on `n`:
* `n = 0`: `0 + 0 = 0` holds by definition;
* `n = k + 1`: `0 + (k + 1) = (0 + k) + 1` by the second rule of addition (`Nat.add_succ`),
  `= k + 1` by the induction hypothesis `ih : 0 + k = k`. -/
theorem zero_add_induction (n : ℕ) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.add_succ, ih]

Lean's library already contains this fact as Nat.zero_add, so we could simply apply it. Both are machine-checked, but they say different things: the first is proved here, from the definitions; the second uses a theorem someone else proved. The Lumenary labels every declaration as independent or library to keep this distinction honest.

/-- The same fact, obtained by *applying* core Lean's theorem `Nat.zero_add`. Both versions are
machine-checked; only the previous one proves it here from the definition. -/
theorem zero_add_library (n : ℕ) : 0 + n = n :=
  Nat.zero_add n

Here is a bigger induction: Gauss's formula $0 + 1 + \dots + n = \frac{n(n+1)}{2}$, stated without division as $2 \cdot (0 + 1 + \dots + n) = n(n + 1)$. We define the sum by recursion and prove the formula by induction; in the inductive step, the tactic ring does the algebra $k(k+1) + 2(k+1) = (k+1)(k+2)$.

/-- `sumUpTo n = 0 + 1 + 2 + ⋯ + n`, defined by recursion. -/
def sumUpTo : ℕ → ℕ
  | 0 => 0
  | n + 1 => sumUpTo n + (n + 1)

/-- **Gauss's formula** `2 · (0 + 1 + ⋯ + n) = n(n + 1)`, by induction. In the step, unfold
`sumUpTo (k + 1) = sumUpTo k + (k + 1)`, distribute, use the induction hypothesis, and let
`ring` finish the algebra `k(k + 1) + 2(k + 1) = (k + 1)(k + 2)`. -/
theorem two_mul_sumUpTo (n : ℕ) : 2 * sumUpTo n = n * (n + 1) := by
  induction n with
  | zero => rfl
  | succ k ih =>
    rw [sumUpTo, Nat.mul_add, ih]
    ring

Much of using Lean is reading statements. Here is Euclid's theorem as Mathlib states it:

theorem Nat.exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p

Read it piece by piece: the name; then the arguments in brackets (for any natural number n); then, after the colon, the statement: there exists p with n ≤ p and p prime. So: for every $n$ there is a prime at least as large as $n$ — that is, there are infinitely many primes. Applying it is one line:

/-- **Euclid's theorem**, read off Mathlib: for every `n` there is a prime `p` with `n ≤ p`.
This applies `Nat.exists_infinite_primes`, whose statement is exactly this. -/
theorem infinitely_many_primes (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p :=
  Nat.exists_infinite_primes n

Statements about general structures have two more kinds of bracket. For instance

theorem add_comm {G : Type*} [AddCommMagma G] (a b : G) : a + b = b + a

says: for any type G (in curly braces: Lean will work out G by itself from a and b), carrying an addition that is commutative (in square brackets: a structure Lean finds automatically — for ℕ, ℤ, ℝ…), and any a b : G, we have a + b = b + a.

Two more library results. The first is certified by norm_num, an automated procedure that checks the arithmetic and hands the kernel a proof to re-check; the second is a famous theorem used as a black box:

/-- `97` is prime, certified by Mathlib's `norm_num` extension for primality (it checks that no
number from 2 up to √97 divides 97, and produces a proof term that Lean's kernel re-checks). -/
theorem prime_97 : Nat.Prime 97 := by
  norm_num

/-- `√2` is irrational: Mathlib's `irrational_sqrt_two`. Here `Irrational x` means that `x`
is not equal to any rational number. -/
theorem sqrt_two_irrational : Irrational (Real.sqrt 2) :=
  irrational_sqrt_two

When Lean accepts a theorem, the kernel has checked that the proof follows from Lean's rules and the axioms listed. That is a very strong guarantee — far stronger than "I read it carefully". But it guarantees exactly that, and nothing more.

1. sorry means "not proved". Writing sorry tells Lean "trust me, I'll fill this in later". Lean accepts the file with a warning, and #print axioms reports that the theorem depends on sorryAx. A proof containing sorry is a plan, not a proof. (The Lean exercises of this lesson are statements with sorry for you to replace.)

2. The check is relative to the axioms and the kernel. Lean's kernel is small and has been studied carefully, and its axioms are standard; but a proof is checked relative to them. That is why the Lumenary shows the axiom list under every declaration.

3. A correct proof of the wrong statement is still a correct proof. This is the most important lesson about formal mathematics. The theorem below is proved correctly:

/-- **A correct proof of a weaker statement.** No *natural number* squares to 2: if `q ≤ 1`
then `q · q ≤ 1`, and if `q ≥ 2` then `q · q ≥ 4`. Lean checks this proof perfectly — but
the statement does **not** say that `√2` is irrational (it says nothing about fractions).
A formal proof is only as meaningful as its formal statement. -/
theorem no_nat_sqrt_two : ¬ ∃ q : ℕ, q * q = 2 := by
  rintro ⟨q, hq⟩
  rcases Nat.lt_or_ge q 2 with h | h
  · have h1 : q * q ≤ 1 * 1 := Nat.mul_le_mul (by omega) (by omega)
    omega
  · have h4 : 2 * 2 ≤ q * q := Nat.mul_le_mul h h
    omega

It says that no natural number squares to $2$. It does not say that $\sqrt 2$ is irrational — that would need "no fraction squares to $2$", which is Mathlib's irrational_sqrt_two above. If someone announced "Lean has verified that $\sqrt 2$ is irrational" on the strength of no_nat_sqrt_two, the checkmark would be genuine and the claim false.

4. Definitions have conventions you must know. Lean's functions are defined for every input, so some familiar operations get unfamiliar conventions:

/-- In Lean, subtraction of natural numbers **stops at zero**: `3 - 5 = 0`, because there is no
natural number `-2`. A statement such as `∀ n : ℕ, n - 1 + 1 = n` is therefore *false* (it
fails at `n = 0`). -/
theorem nat_sub_truncates : (3 : ℕ) - 5 = 0 := rfl

/-- Division of natural numbers **rounds down**: `7 / 2 = 3`. -/
theorem nat_div_rounds_down : (7 : ℕ) / 2 = 3 := rfl

/-- In Mathlib, `x / 0 = 0` for real numbers — a convention that makes division a total
function. So `1 / 0 = 0` is a theorem (`div_zero`), and a statement like "`x / x = 1`" needs
the hypothesis `x ≠ 0` to be true. -/
theorem real_div_zero : (1 : ℝ) / 0 = 0 :=
  div_zero 1

So the statement ∀ n : ℕ, n - 1 + 1 = n is false in Lean (it fails at $n = 0$), and "$x / x = 1$" needs the hypothesis $x \ne 0$. These conventions are harmless once you know them — and dangerous if you don't.

5. Impossible hypotheses prove anything. A theorem whose hypotheses can never all hold is true and useless:

/-- **A vacuous theorem.** If `n + 1 = 0` then `n = 37`. The hypothesis can never hold (a
successor is never zero), so the theorem is true — and useless. Impossible hypotheses make
anything provable; always check that a formal statement's hypotheses can actually happen. -/
theorem vacuous (n : ℕ) (h : n + 1 = 0) : n = 37 :=
  absurd h (Nat.succ_ne_zero n)

So when you read a formal theorem, ask: Is this statement what was claimed? Can its hypotheses actually happen? Which axioms does it use? The machine checks the proof; checking the statement is the human's job.

"""A tiny proof checker for addition of natural numbers.

Lean's kernel is a small program that checks every step of a proof. This
experiment builds a toy version for one theory: natural numbers written with
0 and S (successor, "plus one"), and the two defining rules of addition,
  A1:  a + 0 = a          A2:  a + S(b) = S(a + b).
A proof is a chain of terms; each step must rewrite exactly one subterm with
one rule (or with a hypothesis, such as an induction hypothesis). The checker
accepts a proof of 2 + 2 = 4, rejects a bogus one, shows why n + 0 = n is
"true by computation" while 0 + n = n gets stuck, and checks both cases of
the induction proof of 0 + n = n. Every verdict is exact; the toy shows how
checking works, but is far simpler than Lean's kernel.

Runs unchanged in the browser (Pyodide) using only the standard library.
"""

import textwrap

ZERO = ("0",)

def S(t):
    """The successor S(t), meaning t + 1."""
    return ("S", t)

def add(a, b):
    """The term a + b."""
    return ("+", a, b)

def var(name):
    """A variable such as n (an unknown natural number)."""
    return ("var", name)

def num(k):
    """The numeral k written as S(S(...S(0)...))."""
    t = ZERO
    for _ in range(k):
        t = S(t)
    return t

def show(t, top=True):
    """Write a term readably: numerals as digits, S(x) for other successors."""
    k, u = 0, t
    while u[0] == "S":
        k, u = k + 1, u[1]
    if u == ZERO:
        return str(k)
    if t[0] == "S":
        return f"S({show(t[1])})"
    if t[0] == "+":
        text = f"{show(t[1], False)} + {show(t[2], False)}"
        return text if top else f"({text})"
    return t[1]

def rewrite_root(t, rules):
    """All (name, result) for rules whose left side matches t itself."""
    out = []
    if t[0] == "+" and t[2] == ZERO:
        out.append(("A1", t[1]))
    if t[0] == "+" and t[2][0] == "S":
        out.append(("A2", S(add(t[1], t[2][1]))))
    for name, (lhs, rhs) in rules.items():
        if t == lhs:
            out.append((name, rhs))
    return out

def one_step(t, rules):
    """All (name, term) reachable from t by rewriting exactly one subterm."""
    results = rewrite_root(t, rules)
    for i in range(1, len(t)):
        if isinstance(t[i], tuple):
            for name, sub in one_step(t[i], rules):
                results.append((name, t[:i] + (sub,) + t[i + 1:]))
    return results

def check_chain(chain, rules=None):
    """Check a proof chain; return (True, rule names) or (False, bad step)."""
    rules = rules or {}
    names = []
    for k, (t, u) in enumerate(zip(chain, chain[1:]), start=1):
        found = [n for n, v in one_step(t, rules) if v == u]
        found += [n + " backwards" for n, v in one_step(u, rules) if v == t]
        if not found:
            return False, k
        names.append(found[0])
    return True, names

def first_step(t):
    """The result of rewriting the outermost, leftmost A1/A2 match, or None."""
    found = rewrite_root(t, {})
    if found:
        return found[0][1]
    for i in range(1, len(t)):
        if isinstance(t[i], tuple):
            sub = first_step(t[i])
            if sub is not None:
                return t[:i] + (sub,) + t[i + 1:]
    return None

def normalize(t, limit=10_000):
    """Apply A1/A2 until no rule applies; return (normal form, steps)."""
    steps = 0
    while steps < limit:
        nxt = first_step(t)
        if nxt is None:
            return t, steps
        t, steps = nxt, steps + 1
    raise RuntimeError("no normal form within the step limit")

def verdict(result):
    """Describe the result of check_chain in words."""
    ok, info = result
    if ok:
        return f"accepted (rules: {', '.join(info)})"
    return f"REJECTED at step {info}"

def main():
    two, n = num(2), var("n")
    proof = [add(two, two), S(add(two, num(1))), S(S(add(two, ZERO))), num(4)]
    ok, names = check_chain(proof)
    print("Proof of 2 + 2 = 4:")
    for t, why in zip(proof, ["start"] + names):
        print(f"  {show(t):<16} [{why}]")
    print(f"  accepted: {ok}")
    bogus = [add(two, two), S(add(two, num(1))), num(5)]
    print(f"Bogus chain 2 + 2 -> S(2 + 1) -> 5: {verdict(check_chain(bogus))}")
    print("  (step 2 is not a single application of a rule)")
    print()
    for t in (add(n, ZERO), add(ZERO, n)):
        nf, steps = normalize(t)
        print(f"Computing {show(t)}: reaches {show(nf)} after {steps} step(s)")
    print("  0 + n is stuck: n is neither 0 nor S(something), so no rule fits.")
    good = all(normalize(add(ZERO, num(k)))[0] == num(k) for k in range(101))
    print(f"0 + k computes to k for every numeral k = 0..100: {good}")
    print()
    print("Induction proof of 0 + n = n:")
    base = check_chain([add(ZERO, ZERO), ZERO])
    print(f"  base case 0 + 0 -> 0: {verdict(base)}")
    k = var("k")
    ih = {"IH": (add(ZERO, k), k)}
    step = [add(ZERO, S(k)), S(add(ZERO, k)), S(k)]
    print("  step case, assuming IH: 0 + k = k")
    print(f"    0 + S(k) -> S(0 + k) -> S(k): {verdict(check_chain(step, ih))}")
    print()
    print(textwrap.fill(
        "Epistemic status: exact. Each verdict is a complete mechanical check "
        "of the given chain, and the 101 numeral cases were all computed. The "
        "checker trusts the induction principle and its two rules without "
        "question, and it is a toy: Lean's kernel checks a far richer logic. "
        "Checking 0 + k for 101 numerals is evidence about 0 + n; the "
        "induction proof is what covers every n.",
        width=78,
    ))

if __name__ == "__main__":
    main()

The checker accepts the proof of $2 + 2 = 4$ and rejects a chain that jumps. It also shows mechanically why $n + 0 = n$ is "true by computation" while $0 + n$ is stuck when $n$ is a variable — the same reason rfl fails in Lean. Checking $0 + k = k$ for the numerals $k = 0, \dots, 100$ is evidence; the two checked cases of the induction proof, together with the induction principle, are a proof. The verdicts are exact, but the toy is far simpler than Lean's kernel, which checks a whole logic, not one theory of addition.

• Gottlob Frege's Begriffsschrift (Germany, 1879) created a fully formal language for logic. Alfred North Whitehead and Bertrand Russell's Principia Mathematica (England, 1910–13) attempted to derive mathematics in such a language by hand — famously taking hundreds of pages to reach $1 + 1 = 2$.
• The first computer proof checkers appeared around 1970: Automath, by N. G. de Bruijn in Eindhoven (Netherlands, from 1967), and Mizar, by Andrzej Trybulec in Poland (from 1973), whose library of formalised mathematics is still growing. Robin Milner's LCF (Stanford and Edinburgh, 1970s) introduced tactics and the small trusted kernel.
• Per Martin-Löf (Sweden) developed the type theory of the 1970s on which many systems build; Thierry Coquand and Gérard Huet created the Calculus of Constructions in France in the 1980s, the basis of Coq (renamed Rocq in 2025) and an ancestor of Lean's logic.
• Landmarks: the four colour theorem checked in Coq by Georges Gonthier and Benjamin Werner (2005); the odd order theorem of group theory (Gonthier and a team, 2012); the Kepler conjecture (Flyspeck, 2014, in HOL Light and Isabelle); the Liquid Tensor Experiment in Lean (2022).
• Lean was started by Leonardo de Moura at Microsoft Research in 2013; Lean 4 appeared in 2021. Mathlib is written by a worldwide volunteer community, and since 2024 Kevin Buzzard has led a project to formalise the proof of Fermat's Last Theorem in Lean.

• Kevin Buzzard and Mohammad Pedramfar, The Natural Number Game — learn Lean by proving the properties of addition and multiplication yourself, in the browser.
• Heather Macbeth, The Mechanics of Proof (2023) — an introduction to proof written for Lean, at this level.
• Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, Theorem Proving in Lean 4 — the official guide to Lean's logic.
• Jeremy Avigad and Patrick Massot, Mathematics in Lean — the next step: real mathematics with Mathlib.
• Daniel J. Velleman, How to Prove It (3rd edition, 2019) — proof techniques on paper, the perfect companion.