How this site is verified

Every theorem on these pages was proved by the Lean compiler, not asserted by the author. This page says exactly what that guarantees, what it does not, and how to reproduce it.

What is checked

The Lean is compiled against a pinned version of Lean (v4.34.0-rc2) and of Mathlib, and a proof that fails to compile does not appear on the site. The chapters quote regions of the compiled files rather than retyping them, so the code you read is the code that compiled.

lake build on its own only warns about an incomplete proof — a sorry does not fail a build by itself. What forbids sorry is an axiom audit: every declaration in the library is checked to depend on nothing beyond Lean’s three standard axioms, propext, Classical.choice and Quot.sound. sorry is not a gap in the bookkeeping; it is an axiom, sorryAx, and a proof that uses it anywhere in its dependency graph is caught.

What is not checked

#print axioms <name> is the same walk, run by hand on one declaration, and it is the tool to reach for when reading someone else’s formalization. It guarantees the proof term is honest. It guarantees nothing about the statement: a theorem with an unsatisfiable hypothesis, or the wrong quantifier order, or ℕ where you meant ℝ, can be completely axiom-clean and still worthless. The “Reading autoformalized Lean” section at the end of each chapter is about that half.

The playground floats; the pin does not

The runnable blocks open the community Lean web editor with its “Latest Mathlib” project, which tracks Mathlib’s master and is rebuilt periodically. The library here is pinned. A proof that compiles here today could, in principle, stop compiling in the playground tomorrow if a Mathlib rename lands before the pin is moved. The library deliberately sticks to long-lived material — Finset, BigOperators, Nat.choose — to make that rare.

If a Check it button errors on code that compiles here, compare the Lean version the playground reports (in its project picker) with the pin above. If they differ, that is why: file it as a correction rather than assuming the mathematics is wrong.

Checking it yourself

git clone https://github.com/ddimmery/MrCLean && cd MrCLean/lean
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
export PATH="$HOME/.elan/bin:$PATH"
lake exe cache get      # prebuilt Mathlib, ~4 GB
lake build              # every file, about a minute once cached

To check a single theorem, open any file under lean/MrCLean/ and add #print axioms <name> after it.

Filing a correction

Every claim on this site traces to a specific theorem in the repository linked in the footer. If something looks wrong — a mistranslated statement, a hypothesis that should not be there, a playground link that no longer compiles — open an issue naming the chapter and the theorem. A correction that includes a counterexample to a stated theorem, a #print axioms result that is not the three names above, or a diff between what the prose claims and what the Lean says is the fastest kind to act on.