Check this yourself
Do not trust us: re-check a proof in your own browser. Nothing is sent anywhere; the checking happens on your computer.
I.The theorem
DanielRootTheorem.root_never_costs_more: for every
c and n with 1 ≤ n, c ≤ n * c. Fixing a mistake once at the root
never costs more than fixing its copy in every layer above it.
Lean wrote out its proof, with every definition and lemma the proof uses, as one file (root_never_costs_more.ndjson, 271 KB). Nanoda, a second proof checker written separately in Rust and compiled to WebAssembly (nanoda.wasm, 425 KB), re-checks that file here. This theorem uses no extra axioms, so it does not lean on Lean's compiler.
II.Run it
A checker that passes everything proves nothing, so try two broken copies too. It must refuse both.
Ready. Click a button.
III.What this does not cover
Only this one theorem has a browser re-check so far. Some of our other Lean proofs use native_decide
(in Tower.lean and StampRule.lean): those trust Lean's compiler to run a computation, not only its kernel, so neither checker
alone vouches for them, and they get no re-check button until they are rewritten to use decide.