Your first Lean 4 proof A five-move walkthrough — no installation, ten minutes.

A LeanDFumt tutorial · runs statically in the browser

A proof assistant is not a solver. It is a witness — it accepts your steps only if each one is legal, and refuses everything else. This page walks through one small theorem so you can feel that machinery from the outside.

What you are about to witness

Lean 4 is a proof assistant developed at Microsoft Research and now maintained by the Lean FRO. Its trusted kernel — the part that actually decides whether a proof is valid — is roughly thirty thousand lines of C++. Everything else in the ecosystem, including all of mathematics that has been formalized in Lean, ultimately reduces to a term the kernel accepts.

You will prove one theorem: for every natural number n, adding zero on the left returns n. It is trivial to believe. Proving it — from the definition of addition, without hand-waving, in a way a machine will check — takes five moves.

The panel below the code, on each step, is a rendering of Lean's InfoView — the pane the assistant uses to tell you which goals remain. Watch that panel. When it says Goals accomplished, the theorem is proved.

The theorem

theorem zero_add
∀ n : Nat,   0 + n = n
for every natural number n, zero plus n equals n

The proof, one step at a time

Step 1 of 5 1 goal remaining
  1. Step 1 — declare the goal 
    theorem zero_add (n : Nat) : 0 + n = n := by
  -- proof goes here
  sorry
    Goals (1)
    n : Nat ⊢0 + n = n

    We name the theorem and state it, then open a by-block — a tactic proof. The keyword sorry is a placeholder promising a proof we haven't written yet. The InfoView shows one open goal: given a natural number n, prove 0 + n = n.

  2. Step 2 — induct on n 
    theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => sorry
  | succ k ih => sorry
    Goals (2)
    case zero
    ⊢0 + 0 = 0
    case succ
    k : Nat ih : 0 + k = k ⊢0 + Nat.succ k = Nat.succ k

    Induction splits the proof in two. The base case asks us to prove the statement when n is zero. The inductive case asks: assuming the theorem already holds for some k — that assumption is named ih, the induction hypothesis — prove it for k + 1.

  3. Step 3 — close the base case 
    theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => sorry
    Goals (1)
    case succ
    k : Nat ih : 0 + k = k ⊢0 + Nat.succ k = Nat.succ k

    rfl — short for reflexivity — closes any goal whose two sides are equal by definition. Lean defines addition so that 0 + 0 reduces to 0 without further work. One goal down; one remains.

  4. Step 4 — unfold the successor 
    theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.add_succ]
    Goals (1)
    case succ
    k : Nat ih : 0 + k = k ⊢Nat.succ (0 + k) = Nat.succ k

    The lemma Nat.add_succ rewrites a + Nat.succ b into Nat.succ (a + b). The rw tactic applies that rewrite left-to-right on the goal. Notice how the shape of the goal changed: we now need to prove Nat.succ (0 + k) = Nat.succ k.

  5. Step 5 — apply the induction hypothesis 
    theorem zero_add (n : Nat) : 0 + n = n := by
  induction n with
  | zero => rfl
  | succ k ih => rw [Nat.add_succ, ih]
    Goals accomplished
    No goals · theorem proved

    Rewriting with ih — our assumption that 0 + k = k — reduces the goal to Nat.succ k = Nat.succ k. Lean discharges that reflexively and closes the proof. The InfoView is empty. Every path through the theorem has been checked.

What just happened

Every step you saw was checked, in real time, against the definitions of Nat, 0, +, and =. No test suite ran. No fuzzer sampled inputs. A verifier reduced the whole proof to axioms of type theory and confirmed that the resulting term type-checks. The theorem is now true not because anyone believes it, but because refusing to believe it would require refuting Lean's kernel — a much harder problem than the one we solved.

This is the atomic operation of formal verification. It scales. Cryptographic protocols, compiler passes, distributed consensus, and — increasingly — AI agent behavior are being proved this way, one theorem at a time. What you just watched is not a toy that only works on toy problems. It is the beginning of the same machinery.

Where to go from here