Learn2Lean

Verified Pen-and-Paper Arithmetic

The arithmetic you learned in school, written as programs and proved correct in Lean 4.

Formal verification has a reputation as specialist work, something for researchers and senior engineers. But the question underneath it is plain enough: does a program actually do what it is meant to? School arithmetic is a good place to start asking, because everyone already knows what the right answer looks like.

The stakes are not academic. A single wrong division once cost Intel around $475 million in recalled chips, and the same kind of proof you'll write here is what now guards processors, compilers, aircraft software and cryptography. The wager of this book is that none of it is specialist magic: if you can follow long division, you can read — and write — a machine-checked guarantee that a program is correct.

Every chapter takes one of these algorithms and works through it the same way: describe the method, implement it as a Lean 4 program, run it a step at a time, then prove it correct for every possible input. You don't need to know Lean to begin. The writing keeps almost every line within reach of someone seeing it for the first time.

• Ch. 0Reading Lean Code & representation The notations and proof steps used throughout, and how a number is stored. ready

• Ch. 1Vertical Addition Column sums, the carry, and the place-value invariant — with exercises. ready
• Ch. 2Vertical Subtraction The same shape with a borrow, and the precondition that the top is at least the bottom — with exercises. ready
• Ch. 3Long Multiplication Partial products and shifts, summed into the result — built on the addition chapter, with exercises. ready
• Ch. 4Long Division The trial-digit search and running remainder, proved to give quotient and remainder — with exercises. ready

• Ch. 5Divisibility Tests Why the rules for 3, 9, and 11 work — digit sums and alternating sums, by modular arithmetic — with exercises. ready
• Ch. 6Euclid's GCD Repeated subtraction as rectangular tiling — the first termination proof and functional induction — with exercises. ready
• Ch. 7The Cube-Root Trick Recovering a perfect cube root from its units digit and leading group — proved correct two ways — with exercises. ready
• Ch. 8Square Roots by Hand The digit-by-digit method, proved to return the integer floor of the root — the hardest chapter — with exercises. ready

• —What you built, and where it goes The ideas you now have, where formal verification scales to, and how to carry on with Lean. ready