Described, implemented in Lean, visualised, and proved correct. repo
mulDigit for the trial product, and Chapter 2's
verticalSub for the remainder. Two things are new. Digits come two at a time, in base 100, and the
trial "divisor" grows with the digit you are testing. The proof is the deepest in the book, so it arrives in four
layers.This is the long-division-looking method for square roots, the one most people are shown once and never quite
keep. It returns the integer square root. For a number a, that is the whole number
q = ⌊√a⌋, together with the remainder r = a − q² left over.
Two moves drive it. First, pair the digits from the right. Long division pulls the dividend down one digit at a time; square root pulls it down two at a time. Squaring a number doubles its digit count, so one root digit answers to one pair of the input. Then, pair by pair from the left, you find the next digit of the root.
Take √1234. Pair it as 12 | 34, and build the root left to right.
First pair, 12. With no root yet, this is the plain question "largest digit whose square fits in
12?" — that's 3 (3² = 9 ≤ 12 < 16 = 4²). Write 3; the remainder is
12 − 9 = 3.
Second pair, 34. Bring it down beside the remainder: 3 → 334. Now the clever step.
Take the root so far, 3, double it to get 6, and look for the largest
digit x making (60 + x)·x ≤ 334. That's x = 5:
65 · 5 = 325 ≤ 334 < 396 = 66 · 6. Write 5; the remainder is
334 − 325 = 9.
The root is 35, remainder 9 — and 35² = 1225, 1225 + 9 = 1234,
with 35² ≤ 1234 < 36². So 35 really is ⌊√1234⌋.
x with x² ≤ 12 is 3;
remainder 3.x with
(60 + x)·x ≤ 334 is 5 (65·5 = 325); remainder 9.Where does (2q·10 + x)·x come from? You have the root's leading part q and are choosing
the next digit x, so the fuller root is 10q + x. Squaring it,
(10q + x)² = 100·q² + (2q·10 + x)·x.
The 100·q² part is exactly what the earlier steps already accounted for. That is why the remainder
was carried and the pair "brought down", a shift by 100. So the new amount this digit removes is
precisely (2q·10 + x)·x. Doubling the root and appending the trial digit is not a trick to memorise.
It is that identity, read straight off.
Nat.sqrt. We instead implement the pen-and-paper method you would do by hand: pair the
digits from the right (working in base 100), and peel off one root digit per pair using the shifting trial divisor
above. Proving that procedure correct — right down to the floor guarantee — is the point, not merely
obtaining the number (see the prologue).Three pieces: pair up the digits, search for one root digit, and a loop that walks the pairs carrying a running remainder and a growing root.
2q·10 + x contains the very digit x being
tried, so it changes on every candidate. The final trimTrailingZeros is Chapter 4's, tidying any
high-place zeros off the root and remainder.Step through the method on any number. Each pair is brought down, the root so far is doubled, and the panel runs
the digit search, laddering through the (2q·10 + x)·x values before it subtracts. Watch the invariant
on the last line. After each pair, the root so far squared is at most the part of the number read so far, and it
is never off by more than the remainder.
Try a perfect square like 10201 (remainder 0), or something lopsided like 9999
(root 99, remainder 198 — the remainder can be as large as 2q, and here it nearly is).
The last proof in the book, and the hardest. Before reading it, try to predict its shape. What must the theorem
claim for it to mean "square root"? Where does the (2q·10 + x)·x subtrahend come from? And what keeps
the whole loop honest?
Each digit removes (2q·10 + x)·x from the running remainder. Which identity justifies that exact
amount?
Besides "root squared fits", the loop maintains one more fact about the remainder at every step. Which one, and why is it needed?
You might state the goal as just "q² ≤ a" — the root squared doesn't overshoot. But q = 0
satisfies that for every a, so on its own it pins down nothing. The floor of the square root needs a
companion bound from above — a < (q+1)², which the maintained r ≤ 2q delivers.
One-sided specifications are a recurring trap: the missing side is exactly where a wrong answer hides. You saw the
same thing in division (the remainder < b half) and gcd (the "greatest" half).
This is the longest proof in the book, so each module comes in two parts. First the argument in plain words: read just these, top to bottom, 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.
Four layers, bottom to top: the digit search returns the right digit; pairing preserves the number's value; the
loop maintains an invariant tying the root and remainder to the input; and the top-level theorem reads off
q = ⌊√a⌋. Each layer leans on the one below, and the loop invariant — the heart — is split into
five short steps you can read one at a time.
Goal states in the tooltips are lightly abbreviated; the shapes are what matter.
Long division brings digits down one at a time; this brings them down two at a time. Why two?
What makes the square-root digit search genuinely different from the division one?
The invariant carries r ≤ 2q alongside the main equation. What breaks without it?
intSqrt_is_floor concludes q² ≤ a < (q+1)². Why is that the right way to say
q = ⌊√a⌋?
Run the method on 625. What does it give?
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 ⟨3,_⟩; the server spells them
⟨3, 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.