Described, implemented in Lean, visualised, and proved correct. repo
You line the two numbers up by their right edge and add them column by column, starting from the units. Whenever a column's total reaches ten or more, you write down its last digit and carry a 1 into the column to its left. The carry is the only thing that crosses from one column into the next. It's what makes a long addition more than a row of separate single-digit sums, and it's what both the program and the proof have to keep track of.
Take 158 + 47. Working right to left, the carry (in
yellow) is the one digit that crosses into the next column:
8 + 7 above, you didn't count up
from 8 seven times — you recalled that it makes 15. That memorised table is the real primitive of hand
addition, so the code takes it as the primitive too: a 100-entry lookup, not Lean's built-in counting of
successors. This is the book's guiding choice — mirror the paper method — spelled out in
the prologue.Addition is built in three layers. Each one is proved correct before the next is placed on top of it.
0 and 1 above are digits; the short proofs that they lie below 10
are left out here for readability. When one list runs out, the algorithm keeps going with an implicit
0. That is how it adds numbers of different lengths, and how a leftover carry becomes a new
leading digit, as in 99 + 1 = 100. In the repo the table also carries two catch-all cases for
values ≥ 10, dismissed as impossible (a Digit is below 10 by construction) — Lean's pattern
checker demands them.Lean also asks for a guarantee that the recursion stops: the measure is the combined length of the two lists, which strictly decreases at every recursive call.
Step through one column at a time and watch the invariant panel beside the grid. That relationship never breaks — and that's exactly why the algorithm is correct.
After the lowest k columns, everything read off the two inputs so far is accounted for by the result
so far plus the carry you are still holding. That carry is worth a full place value
10ᵏ, because it belongs to the next column:
aₖ + bₖ = resultₖ + carry × 10ᵏ.
This is the invariant. Each column re-establishes it, so it holds all the way to the end,
where no digits and no carry remain and it collapses to exactly a + b = result. Correctness here
doesn't mean "it looks right on examples." It means "this one relationship is preserved at every step, and it
says what we want at the finish."
Same three layers as the algorithm — but here each layer comes in two parts. First the argument in plain words: read just these and you'll understand why the algorithm is correct. 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.
In the Lean, goal states in the tooltips are lightly abbreviated — · for *, and c' names this column's carry-out — the shapes are what matter.
Note the theorem reads the carry the other way round from §3. There the carry was waiting to enter the
next column, worth 10ᵏ of the whole number; here the theorem speaks about the columns still
to come, where the incoming carry is worth exactly one unit at the current column. They are two views of
the same bookkeeping — multiply the theorem's statement for a tail by 10ᵏ and you recover
the §3 panel.
The invariant, and the algorithm
Let aₖ, bₖ, rₖ be the numbers formed by the lowest k digits. After k
columns, which is always true?
↑ Step the visualiser in §3 — you'll see this exact equation hold after every column.
Right — a number is a list of digits, so you induct on the list. One subtlety:
generalizing carry in the proof above.Watch the tempting but wrong invariant aₖ + bₖ = rₖ (carry forgotten) as you step:
addDigitsPick two digits and a carry-in, predict the (digit, carry-out) the column returns, then reveal the
table lookups it actually does.
addDigits
addDigits does up to two table lookups — first a + b, then sum + 1 if a
carry came in — and reports a carry-out when either did (c1 || c2). Can both be true at once?
Which inputs make the result longer than both of them?
The recursion of verticalAdd terminates. What convinces Lean?
Reading the proof
The proof inducts on a, and again on b inside each case. Why this nested, two-list
structure?
addTable_correct is proved by fin_cases (all 100 digit pairs), yet
verticalAdd_correct is proved by induction. Why the different technique?
A worksheet. Each cell has a starting goal with a gap for you to fill. Press Run 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. The first run is
slow: Lean is cold-loading Mathlib.)
⊢ line means your tactics ran but something is still left to
prove — read the goal after the turnstile. “type mismatch” means a term of the wrong shape (often a
missing argument, or a value where a proof was wanted). “unknown identifier” is a typo or a lemma not in
scope. “ring failed” / “linarith failed” means that tactic couldn't finish — usually it needs a rewrite
first, or it isn't the right tool. The message names the line; start there, and read the goal state, not
just the red text.The real, machine-checked proof is exactly the one in §4 — clone the repo and run it in VS Code.