Proof Paths

Lean is a program that checks mathematical proofs. It tells you whether a proof is correct, but not whether it is any good. Step through real Lean proofs, see what a theorem rests on, find out why two proofs of the same fact can be genuinely different, then play a game where the shortest proof is usually a lemma someone already proved.

Lean in four ideas

1A statement is a goalTo prove a < c, Lean shows you a goal: what you may assume above the line, what you must show after ⊢.
2A tactic is a moveEach line of a proof is a tactic. It turns the current goal into smaller goals, or closes it.
3Lemmas are reusableA proved theorem can be cited by name. One citation can replace a whole argument.
4Lean is the judgeWhen no goals are left, Lean's small trusted core rechecks the whole proof. Nothing gets in on trust.

How Lean reads a proof

Real proofs, one tactic at a time. The goal panels show exactly what Lean showed. Keys: ← →.

The proof

Goal before this step

Goals after

Does it matter which proof you wrote?

To Lean, no. In homotopy type theory, it can.

Lean: any two proofs are the same

Lean only records that a statement is proved ("proof irrelevance"). Which proof you wrote leaves no trace in the mathematics. That is why a 40-line proof and a one-line citation look identical to Lean, and why judging proof quality is left to us.

Homotopy type theory: a proof is a path

Here a proof that a = b is a path from a to b. Two proofs count as the same when one path can be slid onto the other without crossing the hole. Drag the round handles. On the same side of the hole the paths deform into each other. On opposite sides they never do, so they are two genuinely different proofs.

Lean 2 had a homotopy type theory mode, but today's Lean and its maths library chose proof irrelevance, so it does not model this. The panel is the idea, not something Lean computes.

What a theorem rests on

Every theorem in two small libraries and the theorems its proof uses, all the way down. Click a box to move to it.

Theorem

this theoremreference libraryAI-style libraryLean core or axiom×k reached by k routes

Shortest path

Prove each theorem by playing tactics. Every move was recorded from Lean, including the ones Lean rejects. Lowest cost wins.

Open goal

0 cost so far

? par

A step costs 1; opaque automation (simp, omega, grind) costs 2. Each lemma costs 1 the first time you use it, then nothing: reuse is free. A move Lean rejects costs 1.

Your proof so far

Moves for this goal 1–9

The proofs come from two small Lean libraries I wrote: a reference library in the style of Lean's maths library, and an "AI-style" library that imitates machine-written proofs, often re-proving things the reference library already has. Every goal, move and error message on this page was recorded from Lean 4 and is replayed here; nothing is simulated.