← Contents · Ch 0 · Ch 1 · Ch 2
Described, implemented in Lean, visualised, and proved correct. repo
addTable and verticalAdd from that chapter. Get comfortable
with the carry and the three-layer idea there before you start here.To multiply two numbers by hand you break the second number apart, one digit at a time. You multiply the whole top number by each digit of the bottom number in turn, producing a partial product. Because a bottom digit in the tens place is really worth ten times its face value, its partial product is shifted one place to the left; the hundreds digit's is shifted two; and so on. Finally you add all the shifted partial products together.
Multiplication, then, is three moves built on arithmetic you already have: the single-digit times table, a way to multiply a whole number by one digit (carrying as you go), and plain column addition to total the partial products. That last step isn't merely similar to the addition chapter; it is the addition chapter, called as a subroutine.
23 × 14
is twenty-three added to itself fourteen times — and we could define it that way in one line. But you never
computed like that on paper, and neither will we (see the prologue's note on this).
The whole point is to verify the method you were taught: the memorised times table, digit-by-digit
multiplication with carries, shifts for place value, and a final column addition. So that is what the code does.Take 23 × 14. Multiply 23 by each digit of 14 in turn; the tens digit's partial product is
shifted one place left (a trailing zero), then the two are added.
The build has three layers, each resting on the one below. The bottom of the stack reaches back into the addition chapter.
0 and 1 above are written plainly; the short proofs that
they lie below 10 are left out for readability. shiftLeft prepends n zeros to the list.
The list is least-significant-first, so a zero at the head of the list is a zero at the END of the
written number — §1's trailing zero, a factor of ten. Termination of mulDigit follows from the digit list getting shorter at each call.Step through one partial product at a time. Each new row is the top number times one digit of the bottom number, slid into its place. The panel tracks the identity the whole algorithm rests on.
Every partial product is the top number times one bottom digit bᵢ, and because that digit sits in
place i it is worth 10ⁱ times its face value. So the answer is the sum of those shifted
pieces:
a × b = Σᵢ (a × bᵢ) × 10ⁱ.
That one distributive identity — multiplication spread across the digits of b, each at its own
place value — is the whole reason the method works, and it is exactly what the final theorem states. The
carries inside one partial product, and the carries inside the final addition, all exist to compute
this sum with digits that never exceed nine.
A single lookup in mulTable returns the (units, tens) of a one-digit product. What does
mulTable 5 8 give?
You have read two of these proofs now, so before unrolling this one, try to predict its shape. The algorithm is new, but the habits carry over: ask what kind of arithmetic the goals will be, which already-proved results you can stand on, and what has to be generalised for an induction to go through. The answers differ from the first two chapters, and where they differ is worth noticing — which is why it pays to ask before you read.
omega finish it, as before?Addition and subtraction closed with omega. This proof multiplies numbers and carries powers of ten
(10ⁱ) around. Will omega close it the same way?
The answer is a sum of many partial products, and the summing is done by verticalAdd — which you
proved correct in Chapter 1. What will this proof most likely lean on?
The sum is proved by induction on the digits of b, and each digit's partial product is shifted by
its position. For the inductive hypothesis to apply to the tail, what should be generalised — the way the carry
was in addition?
It is a chain of short lemmas, each one built on the one before. Every step comes in two parts. First the argument in plain words: read just these, top to bottom, and you'll see why long multiplication 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 a column's carry-out — the shapes are what matter.
Long multiplication rests on one equation — the one the final theorem proves. Which is it?
The partial product for the bottom digit in place i is slid left by i positions before being added. Why?
shiftLeft puts the zeros at the HEAD of the list. Why is that the right end?
Inside mulDigit, processing one digit does a times-table lookup and then two
addTable steps. Why does a single column need carries from two places combined?
addTable and subTable returned Digit × Bool, but mulTable
returns Digit × Digit. Why the richer type?
mulDigit_correct begins with set_option maxHeartbeats 0 — something the table proofs
in addition and subtraction never needed. Why here?
A worksheet. Each cell has a starting goal with a gap for you to fill; press Run and your code is
compiled by Lean 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.
The _ proof holes shown in the cells are spelled by omega on the server, as in §2.
(Requires the checker server — see web/checker/README.md. The first run is
slow: Lean is cold-loading Mathlib.)
The real, machine-checked proof is exactly the one in §5 — clone the repo and run it in VS Code.