Described, implemented in Lean, visualised, and proved correct. repo
verticalSub, and that chapter's correctness theorem is what convinces Lean the recursion stops.
Two ideas are new here. It is the first algorithm whose termination Lean does not hand us for free, and its
proof uses an induction shaped like the function rather than like a list.Picture two numbers, 48 and 36, as the sides of a rectangle. Now a tiling question about it: what is the largest square that paves the whole rectangle exactly, leaving no gaps and no overhang, every tile the same size?
Euclid's answer is to carve. If the rectangle is already a square, its side is the answer. If not, cut off the biggest square you can — one as wide as the shorter side — and ask the same question about the strip left over. Cutting a 36 × 36 square from a 48 × 36 rectangle leaves 12 × 36, and in arithmetic that cut is just subtracting the shorter side from the longer. Keep carving, and the square you finally land on has the answer for its side.
Why does the answer survive each cut? A square of side s tiles a rectangle exactly when
s divides both sides. And the common divisors of a and b are
exactly the common divisors of a − b and b: anything dividing both sides divides
their difference, and anything dividing the difference and one side divides their sum. So each cut changes
the rectangle but not the question's answer:
gcd(a, b) = gcd(a − b, b) whenever b ≤ a.
That single equation, applied until the two numbers agree, is the whole algorithm.
gcd(a, b) with gcd(b, a mod b) — fewer steps, but a mod hides a whole
division inside each step. We use the older subtractive form, gcd(a, b) = gcd(a − b, b),
because it is the one you can actually see: repeatedly carving the largest square tile off a rectangle. The
correctness and the tiling picture fall out of the same equation. It is slower, and that cost is exactly what
surfaces as the termination proof in §2.Just one recursive function this time, but it asks something the earlier chapters never did. Those walked down a list, so Lean could see for itself that the recursion stopped. Here the arguments are plain numbers that shrink by subtraction, and Lean won't take termination on trust: you have to give it a measure and show the measure falls at every call.
gcd 0 n = n — and they are load-bearing.
Starting from two positive numbers the recursion never reaches a 0 (subtracting the smaller from the strictly
larger keeps both positive), but a Lean function must be defined on every input, and without the guard
gcdSub 0 5 would subtract 0 forever, making no progress.Step through the carving. Blue squares are already removed, the orange square is being removed now, and the faint region is still to do. The panel tracks the invariant that makes it all work: the gcd of the leftover rectangle's sides never changes. The last step re-tiles the whole rectangle with the answer.
Try lopsided sides too, like 144 × 5. The carving crawls, because subtractive Euclid peels off one
small square at a time. That is the inefficiency the usual remainder version fixes, trading a long run of
subtractions for a single a mod b. The proofs only care about correctness, though, and the slow
version is the honest, geometric one to reason about.
Six chapters in, you know the routine: before reading the proof, try to predict its shape. What should the statement say? What one fact does each recursive step lean on? And, new this time, why does the recursion stop at all?
Each recursive call replaces (a, b) by (a − b, b). Why is that allowed to leave
the answer unchanged?
The recursion doesn't consume a list — both arguments stay as long as they like. What convinces Lean it terminates?
It is tempting to say the gcd is simply "a number that divides both a and b." But
1 divides both — and so does every other common divisor — so that test is passed by many numbers,
most of them wrong. A correct specification needs two clauses: the result divides both sides, and it is
the greatest such number (every common divisor divides it). That is exactly what gcdSub_tiles
states; "divides both" alone would let a lazy algorithm return 1 every time and still look correct.
Two theorems, and each comes in two parts. First the argument in plain words: read just these and you'll see why the algorithm is correct and why it deserves the name gcd. Then, folded underneath, the full Lean proof, for anyone who wants the machine-checked details. You can follow the whole chapter without opening a single dropdown.
The proof brings in one new tool: functional induction. Every recursive function Lean accepts
comes with its own induction principle, shaped to match the function's case-split.
induction a, b using gcdSub.induct hands us five goals, one per branch of the definition, and in
the two recursive branches it gives us the inductive hypothesis right where the recursive call sits. Nothing is
peeled off a list; the recursion itself is what we climb.
Goal states in the tooltips are lightly abbreviated; the shapes are what matter.
Starting from two positive numbers, can the recursion ever reach a 0?
induction a, b using gcdSub.induct — what exactly does it produce?
verticalSub_correct' appears in two different roles in this chapter. Which two?
Roughly how many recursive steps does gcdSub take on gcd(1 000 000, 1)?
What does gcdSub return on gcd(14, 21), and how does it get there?
gcdSub_tiles proves two things: the answer divides both sides, and every common divisor divides the
answer. Why isn't the first half enough on its own?
Suppose you deleted the toNat a = toNat b branch, leaving only the two subtraction branches. What
happens?
A worksheet. Each cell has a starting goal with a gap for you to fill. Press Run (or Ctrl+Enter
in the cell) and Lean compiles your code on the server. Run all checks every cell in turn,
Reset all restores the blank cells, and every cell hides a reference solution you can reveal
once you've tried. (Requires the checker server — see web/checker/README.md.
In the listings digit literals may be shown as ⟨8,_⟩; the server spells them
⟨8, by omega⟩. The first run is slow: Lean is cold-loading Mathlib.)
The real, machine-checked proofs are exactly those in §5 — clone the repo and run them in VS Code.