This chapter's code examples and dropdowns are rendered by JavaScript — with it disabled you will only see the prose. The full Lean source is in the repo.

Chapter 0 · Reading Lean Code

How to read the code in this book, the proof steps it uses, and how a number is represented · source

Every chapter of this book follows the same path. It describes a school arithmetic algorithm, shows the algorithm written as a Lean 4 program, lets you run it a step at a time, and then proves the program correct for every input, not only the examples you happen to try. Some chapters end with small exercises you can check in the browser.

This book assumes you have never written a line of Lean. The chapter you are reading is the one bit of groundwork before the algorithms start: it gathers the few notations and proof steps that turn up everywhere, and it explains how we store a number. Read it once and the rest should follow.

Wherever code appears, you can hover a highlighted name or tactic for a short explanation. Inside a proof, the hover also shows the goal still left to prove at that point. One convention to know: the hover shows the goal remaining after that step runs — except for closing tactics, which show the goal they close. It is a stripped-down, offline version of the live view Lean gives you as you work. There is a toNat further down to try it on.

One proof, every input Notations Tactics Representing a number A first proof

One proof, every input

Testing an algorithm runs it on a handful of inputs. A proof settles every input at once — including the ones no one thought to try, which is exactly where real bugs hide. Checking that 7 + 8 = 15 a thousand times tells you nothing about the thousand-and-first case; a proof rules the whole infinity out in a single stroke. That gap between "works on my examples" and "works, always" is the difference this book is built on.

One caveat comes with the power. A proof only ever certifies what you actually asked it to — the specification, the precise statement of what "correct" means. State that wrongly and a flawless proof will faithfully certify the wrong thing, so half the craft is choosing the right property to prove. Several later chapters come back to exactly this: telling a genuine specification from a plausible-but-weak one.

The notations

The code is Lean 4. Only a handful of notations come up repeatedly; the list below gathers them, so you can read the definitions and proofs without having met the language before.

def f := …Introduces a function or value named f. abbrev N := …Names an abbreviation for an existing type — e.g. Digit for Fin 10. theorem T : … := by …States a claim (after the colon) and gives its proof (after by). example : … := by …The same as a theorem, but unnamed — used for one-off checks and the exercises. Fin 10A whole number between 0 and 9. This is what we call a Digit. BoolA true/false value. Here it records whether a column produced a carry or a borrow. A × BA pair: one value of type A and one of type B. A column adder returns a digit paired with a carry. p.1, p.2The first and second halves of a pair p. For a column adder, p.1 is the digit written down and p.2 the carry. f : A → BA type annotation: f takes an A and returns a B. Chained arrows (A → B → C) mean a function of two arguments. []The empty list. x :: xsA list whose first element is x and whose remaining elements are the list xs. A number is stored as such a list of digits. | pattern => resultOne case of a definition: when the input has the shape pattern, the answer is result. Giving cases for [] and x :: xs is how a function over lists is defined. | n + 1 =>A pattern that matches any number ≥ 1 and names the number one below it n. Together with | 0, it covers every natural number. let (d, c) := …Names the two halves of a pair, so they can be used separately on the next line. d.valThe plain number carried by a digit d (the 7 inside the digit 7). ⟨0, by omega⟩A digit written out in full: the value 0 together with a short proof (by omega) that it is a valid digit — that is, below 10. Because the proof travels with the value, an out-of-range digit can never be formed. a + 10 * b, ≤Ordinary addition and multiplication, and "less than or equal to". calc a = b := by … _ = c := by …A chain of equalities read top to bottom, each step justified on the right; the underscores repeat the previous line's right-hand side. Used in later chapters. ⊢ …Shown in a proof tooltip. It is the statement that still remains to be proved at that point.

Tactics — the steps inside a proof

A Lean proof is everything after by: a list of tactics. Each one takes the current goal (the statement still to be proved) and turns it into something simpler, and the proof is done when no goals are left. You never have to write any of this to read along, since the proofs explain each step in place. For the exercises, these are the moves you choose from.

Each tactic below comes with a tiny example of its own, nothing to do with our algorithms, just enough to show the shape of what it does.

Two symbols stitch tactics together. Writing t1 <;> t2 runs t2 on every goal that t1 left behind. That is the trick in fin_cases a <;> fin_cases b <;> simp …, which fans out into 100 goals and shuts them all in a single line. Adding at * to a tactic, as in simp … at *, points it at the hypotheses too, not just the goal.

Representing a number

Before we can prove anything about an algorithm, Lean has to be told what a number even is. We store one as the list of its digits, least significant first, so 1239 is held as [9, 3, 2, 1]: units, then tens, then hundreds, then thousands. A single digit, a value from 0 to 9, is a Digit; a list of them is a MultiDigit.

One function ties this representation back to ordinary numbers: toNat reads a digit list and returns the number it stands for.

The second line reads: the value of a list is its units digit, plus ten times the value of everything above it. This one function runs through the entire book. Every algorithm's correctness theorem is phrased in terms of toNat, because that is how you say precisely what you mean, that the digit list an algorithm hands back stands for the right number.

The least-significant-first order matches how the algorithms actually run: units column first, the way you do it by hand. That alignment keeps the recursion and the proofs simple.

Why it's built this way. A guiding rule runs through the whole book: model the pen-and-paper method, as faithfully as the code allows — not whatever shortcut a computer would prefer. Lean already knows that a natural number is zero-or-a-successor, and it would happily let us define addition by counting up one at a time, or multiplication as repeated addition. But that is not what you did at a desk. You never added 8 and 7 by ticking up fifteen times; you recalled that 8 + 7 is 15, carry the 1 — a memorised table plus a place-value rule. You knew multiplication was repeated addition, yet you never used that fact to compute; you leaned on the times table and shifted columns. So here addition and multiplication are built from small look-up tables applied column by column, division from a trial-digit search, square roots from digit pairs — each algorithm mirroring the hand method it is named after. The payoff is that when we prove one correct, we are proving that the schoolbook procedure itself is sound, not merely that some equivalent arithmetic exists.

Two habits show up again and again, and together they explain the general shape of the proofs to come. The first: a digit is a Fin 10, so it is below 10 by construction. There is no separate validity check to drag around, and the odd table case that would need a digit of 10 or more cannot arise, so it is dismissed on the spot. The second: the tactic omega handles routine arithmetic by itself, bounds and carry conditions and the like. Leaning on it frees each proof to deal with the real structure of the algorithm, the induction and the place-value identity, rather than grind through calculation.

A first proof

Every result in this book is proved with tactics like the ones above. The earliest proofs in the project are about toNat itself, and they are short enough to read start to finish, a good look at what a Lean proof is really like before the algorithms arrive. (Hover any highlighted step for its meaning and the goal left at that point.)

The first two facts just restate the two defining cases of toNat, so each holds by definition. rfl checks that the two sides compute to the very same thing, and that is all it takes.

Reading a digit list as a number is only half of it; we want to go the other way too. fromNat builds the digit list for a number, stripping off the units digit with % 10 and recursing on what is left with / 10.

Note the base case: zero is encoded as the empty list, and fromNat never writes leading zeros. That is also why the round trip is stated in this direction — [0, 4] and [0, 4, 0] both read back as 40, so encoding a number and reading it back is exact, while reading a list and re-encoding it may drop redundant zeros.

The two should undo each other: encode a number, read it back, and you land on exactly what you started with. That is the first real theorem in the book, and the first real induction. If you've not met induction: it is the one move that lets a finite proof cover infinitely many numbers — show the claim for the base case, then show that if it holds for the smaller number it holds for the next, and those two together pin it down for every number at once. Every correctness proof in this book is built that way.

Its shape is the shape every correctness proof in this book will take: induct, rewrite with the definitions, apply the inductive hypothesis to the smaller number, then hand the leftover arithmetic to omega. One wrinkle turns up right away. Because fromNat recurses on n / 10 rather than n − 1, the proof needs strong induction: the flavour that gives you a hypothesis for every smaller number, not just the one directly below.

Want to run any of this yourself? Clone the repo, then lake exe cache get (this pulls down a prebuilt Mathlib, so you are not left compiling it) followed by lake build. The end-of-chapter Lean worksheets also need the checker server; that lives in the repo under web/checker.