← Contents

Epilogue

What you built, and where it goes from here.

Eight chapters ago the pitch was that formal verification only sounds like specialist work. If you made it here, you've now done it — on arithmetic you've known since primary school, but done properly.

What you actually did

You took the algorithms everyone learns by hand and wrote each one as a Lean program: the carry in addition, the borrow in subtraction, partial products in multiplication, the trial-digit search in division, the digit tests for divisibility, Euclid's rectangle-carving gcd, and two mental "tricks" that turned out to have real theorems hiding inside them.

Then, for every one, you did the thing that makes it verification rather than programming: you proved it correct — not checked it on a few examples, but showed it gives the right answer for every input there is. And these aren't proofs you have to take on trust. Lean's kernel checked each one, and it would have rejected a single wrong step. The green checkmark means the machine agrees.

Along the way you met the ideas that carry all of formal verification — each introduced in one chapter, then used again and again:

• a specification — what "correct" even means (the toNat correspondence, from Chapter 1 on) — and the harder skill of telling a right spec from a plausible-but-weak one (Ch 4, 6, 8);
• an invariant that holds at every step of a loop — the carry in Chapter 1, value = q·b + r in 4, r ≤ 2q in 8;
• a precondition that must be assumed and re-earned (b ≤ a, b ≠ 0);
• induction to reach past the finite examples to all inputs at once — and generalizing the statement so the induction goes through (the arbitrary carry);
• termination, shown by a measure that strictly shrinks (Chapter 6);
• composition, building a verified operation from verified pieces (multiplication on addition), and the choice between a brute-force and a structural proof of the same theorem (Chapter 7).

None of these change when the programs get serious.

Where this goes

The same move — state a specification, prove the implementation meets it — scales a very long way:

• Hardware. After the 1994 Pentium division bug cost Intel about $475 million, chip makers began proving their circuits correct; Intel, AMD and Arm now formally verify floating-point and other arithmetic units before the silicon ships.
• Compilers & languages. CompCert is a C compiler proved to preserve the meaning of the programs it compiles, so compilation can't introduce bugs the source didn't have.
• Operating systems. seL4 is a microkernel proved correct down to its C implementation, now used where failure isn't an option — aircraft, medical devices, defence.
• Security. Verified cryptography — the routines shipping in Firefox and Chrome — is proved to match its mathematical spec, because a subtle bug there is a security hole.
• AI & autonomy. Researchers now prove properties of the neural networks used in safety-critical control — that an aircraft collision-avoidance network, for instance, never advises an unsafe manoeuvre within a modelled envelope.
• Mathematics. Mathlib, the library your later chapters leaned on, is a growing, machine-checked formalisation of modern mathematics, built by hundreds of people in the language you just used.

The distance between what you did and those projects is size and stamina, not kind. The omega and induction you called are the same tactics; the rectangle only got bigger.

Carrying on with Lean

If the folded-away Lean proofs pulled at you rather than put you off, these are the routes that fit best coming from this book:

• The Natural Number Game — build the natural numbers and their arithmetic from nothing, in the browser. The gentlest start, and the closest in spirit to what you just did.
• Glimpse of Lean — a short, hands-on tour you work through in your own editor: the fundamentals first, then a taste of real analysis, topology and logic. A natural next step once the game clicks.
• The Mechanics of Proof — a gentle, well-paced course in writing proofs in Lean; the best next book if you don't have much university mathematics behind you.
• Functional Programming in Lean — Lean as a programming language, for readers who came at this from the code side.
• Theorem Proving in Lean 4 — the official book, when you want the language and its foundations properly.
• the Zulip chat — where Mathlib is built, and a welcoming place to ask a first question.

Thanks for reading. You came for a party trick or a curiosity about proofs, and you leave able to read — and write — a statement that a program is correct, and to know the difference between believing it and proving it. That's the whole game.

The Lean community keeps a fuller, always-current catalogue of tutorials, games and books at leanprover-community.github.io/learn — start there whenever you want the complete map.