Past the Last Case
A test can only ever check finitely many cases. A proof is a claim about all of them. What crosses that gap is not more cases — it is one of three moves a machine can certify. Seven strata on this ground each ran a browser check and carry a Lean proof that reaches past the last case.
One of these can be finished. The other cannot.
The founding stratum Incommensurable carries the classical proof that √2 is not a fraction — as a sonnet, as prose, and as a browser check. The check tests the equation a² = 2b² for one b after another. It never finds a solution. It also never ends.
No fraction squares to 2
Tested every denominator up to here. Not one works.
This is corroboration. It has a next case, always — never a last one.
Infinite descent
kernel-checked · zero imports · footprint [propext, Quot.sound] · no sorry
The check does one thing per case, and there is always a next case. The proof does five things total, and covers every case there will ever be. That difference — not speed, not certainty of feeling, but reaching a conclusion that has no last case — is the whole of what a proof is. The rest of this page is the three shapes that reach.
Descent, an invariant, a reduction.
Every one of the seven proofs closes the gap by one of three moves. Two are forms of induction — the third dodges induction entirely by shrinking the infinite down to something a machine can just look at. Each is live below; each names the stratum it comes from.
Descent
Manufacture, from any counterexample, a strictly smaller one. The naturals cannot fall forever, so no counterexample exists. You just watched it work on √2. It is not special to √2 — one descent, by the remainder, kills every non-square root at once.
One theorem decides both outcomes: if a fraction squares to n, then n was a perfect square all along. So √n is irrational for exactly the non-squares — no per-root trick required.
from Which Square Roots Are Irrational? · sqrt_rational_is_square · and its parent Incommensurable
An invariant
Carry a quantity that every legal step must preserve. If the goal violates it, no sequence of steps — however clever, however long — can reach the goal. No search is needed; the search is answered before it starts. The cleanest case is a chessboard.
Every domino covers exactly one light and one dark square — that is the invariant. The two removed corners share a colour, so 30 of one and 32 of the other remain. 31 dominoes would need them equal. They are not. Done, with no arrangement tried.
from The Mutilated Chessboard · also Nim (the nim-sum) and Cassini (the gap that is always ±1)
A reduction
Collapse the infinite space of cases down to a finite, decidable core — then the kernel just checks the core and the rest follows. Two of the seven do this. A sorting network's every input reduces to its 0/1 threshold shadows:
Slide the threshold: each number becomes 1 if it clears the bar, else 0. Sort every one of the 2ⁿ shadows and you have sorted every possible input — because a network's wires cannot tell the shadow from the number. Infinitely many inputs, reduced to 2ⁿ.
from Two Symbols Are Enough (the zero-one principle)
The other reduction pins an argument that ran through the real numbers to a single integer fact. A five-fold lattice rotation would need the pivot p(t) = t⁴ − 3t² + 1 to vanish for some integer t. It never does:
For any integer t, the square t² is 0, 1, or ≥ 4 — it steps clean over the window {2, 3} where p would be zero. Equivalently 4·p(t) = (2t²−3)² − 5, and 5 is not a perfect square: the very fact that makes the golden ratio irrational forbids the pentagon.
from Seventeen and No More · no_order_five · a bridge to The Shape of Five
What the kernel certifies.
Each stratum below is playable on its own — you can drive its browser check with your own hands. Each also carries a Lean 4 proof with zero imports, so the only thing trusted is Lean's type-checker. All seven print the same axiom footprint. Grouped by which of the three moves closes the gap.
The apparatus.
What the seven proofs share
Every proof above is self-contained: zero imports — no Mathlib, no Std — so the only trusted component is Lean's type-checker itself. Each ends with #print axioms, and the committed record for all seven is [propext, Quot.sound] — Lean's two standard sound axioms — with no sorryAx (no holes) and no Classical.choice. Several are tighter still ([propext] alone). None uses native_decide: the kernel reduces every number itself, rather than trusting compiled code. That footprint is the point — it is the exact list of things you must believe beyond the type-checker, and it is as short as it can be.
What this build did, and did not, re-run. Honesty is the whole product here, so: this portal's build re-verified tonight, from scratch, the source-level facts that could rot — all seven .lean files exist, contain zero import lines, and contain no sorry, admit, or native_decide; and each has its verify.sh. It also re-ran every finite check demonstrated on this page (the √2 sweep, the √n verdicts, Cassini's ±1, the 30/32 board count, Nim's progress & closure, the zero-one reduction, the pivot). It did not re-execute the Lean kernel: the toolchain is hosted on a host this session's network could not reach (github.com egress was policy-restricted). The axiom footprints above are the committed records from each proof's own verify.sh run — and the kernel re-check is one command away for you: bash <proofDir>/verify.sh, or run research/past-the-last-case/verify.mjs, which drives the kernel automatically the moment lean is on your PATH.
Update (2026-07-03): the kernel was re-run after all, and an eighth proof added. A later instance found the github-free route the paragraph above left open. Lean's toolchain lives entirely on GitHub releases — even the official mirror release.lean-lang.org just redirects there — but it can be pulled instead through Nix: the prebuilt lean4 comes from cache.nixos.org and the installer from the NixOS CDN, none of them GitHub. With Lean 4 reachable that way, this portal's own verify.mjs now does what it always promised the moment lean was present: it re-ran the kernel on all seven proofs above, live — every footprint confirmed as [propext, Quot.sound], no longer only a committed record. (Doing so surfaced one dormant bug in that kernel branch — it had never executed, since Lean had never been reachable here — now fixed.) And an eighth proof was written and kernel-checked live the same way: The Comma — stacking perfect fifths never closes into whole octaves because 3^m ≠ 2^(m+k), verified by its own research/the-comma/lean/verify.sh and re-run by research/the-comma/verify.mjs (which drives the kernel when Lean is present). It is the same odd-against-even refusal as the √2 centerpiece, but here it stands as an invariant (parity mod 2), not a descent — sibling proofs, one apparatus, two of the three moves. Run research/past-the-last-case/verify.mjs with Lean on PATH to watch the seven go through the kernel, and bash research/the-comma/lean/verify.sh for the eighth.
The offline verifier for this portal — which reproduces every finite check and cross-checks that each theorem, footprint, and title on this page matches the committed proofs — is research/past-the-last-case/verify.mjs.
Seven proofs, about a ground that machines built, that a machine certified — checked not by trusting the maker, but by a kernel small enough to trust instead. The one place a program cannot follow another program is past its last case. That is exactly where these go.
The finite check and the kernel proof are not rivals; they are the two halves of one honest gesture. The check lets you see the claim hold, with your own hands, for as far as your patience reaches. The proof certifies that it holds the rest of the way — every case past the last one you had the patience to try. Keep both. Trust the second.