The book opened with Greeks inventing proof-by-argument. It closes with proofs that type-check, champions crowned by online amateurs, and neural nets whispering conjectures. The 2,300-year arc bends back to your terminal.
Twelve chapters ago a Greek with a scroll asked a question nobody had bothered to ask: how do you know? Every era since answered with a bigger toolbox. This chapter is where the toolbox grows a CPU.
Four stories, one theme: the wall between "doing mathematics" and "running programs" is dissolving — and it's dissolving in both directions. From one side, proofs are becoming programs: you don't read them and nod, you compile them and the machine refuses to lie. From the other, programs are becoming mathematicians: neural nets trained on tables of data spot patterns no human noticed, then hand humans a conjecture to prove.
We'll meet a number system that falls out of analyzing board games, a 47-million-step Turing machine crowned by hobbyists with a theorem prover, a 1.5-million-line library of mathematics that a compiler checks line by line, and a machine that points at a wave in the data and says "look here." Four map fields: surreal numbers & combinatorial game theory, busy-beaver / the limits of computation, formalized mathematics, and machine-learning as a mathematical collaborator. Three widgets, one code card, one quiz, one ending.
And here's the secret the whole book has been keeping from you, dear Scala-writing, Haskell-curious reader: it was always about your day job. The recursive datatype, the type that's a proof, the function that out-grows all functions — they were on the map the entire time. Let's collect the payoff.
In 1974 John Conway published On Numbers and Games, and in 1982 he and two co-authors followed it with Winning Ways. The setup sounds like recreation: sit down and analyze the endgames of simple two-player games. The punchline is that an entire number system falls out of the analysis — and it's bigger than the one you learned in school.
Here's the move. Every position in these games has a value. Define that value recursively: a game is just two lists of games — the positions Left can move to, and the positions Right can move to. Write it { L | R }. That's the whole datatype. Now watch numbers appear out of nothing:
{ | } = 0 — neither player has a move. Empty lists. This is zero.{0 | } = 1 — Left can move to 0, Right is stuck. One move of advantage to Left: the value 1.{0 | 1} = ½ — Left's best leaves 0, Right's best leaves 1. The value wedged exactly between: one half.Keep going and you don't just get the fractions. You get all the real numbers — every √2 and π — and then you keep going past them: infinite numbers larger than any integer, and infinitesimals smaller than any positive fraction but bigger than zero, nestled in the cracks. Conway called the whole collection the surreal numbers. Donald Knuth liked the idea so much he wrote a novella about it — and coined the name "surreal" in the process. A number system, discovered inside a novel, born from playing games.
And the construction — the part a functional programmer should feel in their teeth — is one recursive datatype with an ordering. That's it. Numbers, all the way down to the infinitesimals, are an algebraic data type.
{ left | right }, with the rule that every left option is strictly less than every right option. The value is "the simplest number strictly between the two sides." 0 is { | }; everything else is built from it.The emotional payoff, in two languages. Back in Chapter 1 we joked that "a number is an algebraic data type" — a multiset of prime factors. Here that joke stops being a joke entirely. Conway's whole number system is a case class:
Where do these values come from, concretely? From games you can play with a pencil. The cleanest is Hackenbush: a picture of colored edges growing up from the ground. Left (blue) deletes blue edges, Right (red) deletes red edges, and when you cut an edge, everything no longer connected to the ground falls off. Whoever can't move loses. Every Hackenbush picture has a surreal value, and the value tells you who wins. Build one below — and watch ½ appear.
In 1962 Tibor Radó asked a deceptively small question. Take all the Turing machines with n states that eventually halt. Among those, which one runs the longest before stopping? Call that number BB(n) — the busy-beaver number. It's the maximum number of steps a halting n-state machine can take.
The first few are tame: BB(1) = 1, BB(2) = 6, BB(3) = 21, BB(4) = 107. Then the floor drops out. BB(5) turns out to be 47,176,870. And BB(n) grows faster than any computable function — faster than anything you could ever write a program to compute. That's not hyperbole, it's a theorem, and it's the same theorem from Chapter 7: if you could compute BB(n), you could solve the halting problem (run a machine for BB(n) steps; if it hasn't halted, it never will). Since halting is undecidable, BB out-runs every program you can write. It is a sequence of perfectly definite whole numbers that no algorithm can keep up with.
Now the part that makes this Chapter 13 and not Chapter 7. For sixty-two years BB(5) was a conjecture. The maximum step count was believed to be 47,176,870 — found by a champion machine — but proving no other 5-state machine ran longer meant proving that thousands of stubborn non-halting machines really never halt, one awkward case at a time. In July 2024 the bbchallenge collective — an online gang of hobbyists, an open repository, and a Coq-verified proof — closed it: BB(5) = 47,176,870, settled, machine-checked.
BB(6) is already off the edge of the map. Its champion is known to run for a number so large it's entangled with statements ordinary mathematics can't decide. Amateurs on a forum, a public git repo, and a proof assistant that doesn't get tired: that's the new shape of mathematical work. The garage below runs the real verified champion. Mind the step counter.
Chapter 7 left us with a strange, beautiful idea called the Curry–Howard correspondence: a proof is a program, and a proposition is a type. A proof of "A implies B" is literally a function from A to B. Back then it was a curiosity logicians traded at lunch. Now it's industrial.
In a proof assistant like Lean, a theorem is a type and the proof is a program that inhabits that type — a value of that type. To check the proof, you type-check the program. If it compiles, the theorem is true. Not "true pending review," not "true modulo the details left to the reader." True. The compiler does not nod politely at a gap; it stops and points at it.
This stopped being a toy. Lean's mathematics library, mathlib, now holds over 1.5 million lines of machine-checked mathematics — definitions, lemmas, and theorems that all type-check together. In 2023 Terence Tao took a paper he'd just finished — the Polynomial Freiman–Ruzsa conjecture (PFR) — and formalized it in Lean with a crowd of online collaborators in about three weeks, partly, he said, to be sure the brand-new proof had no holes. Maryna Viazovska's sphere-packing proof from Chapter 10 — the eight-dimensional miracle — has been formalized too. The frontier of research and the compiler now meet in the same week.
You don't need to know Lean to read one. Here's a complete, real proof in Lean 4 that addition on natural numbers commutes — that a + b = b + a. Look at it, then read the narration.
Line by line, in plain English:
theorem add_comm' (a b : Nat) : a + b = b + a — the type. It says: for any two naturals, these two sums are equal. Everything after := must produce a value of this type, i.e. a proof.by — enters tactic mode. Instead of writing the proof term by hand, you'll issue commands that build it for you.induction b with — split into cases. Prove it when b is zero, and prove it for succ n (i.e. n + 1) assuming it already holds for n (the induction hypothesis ih).| zero => simp — the base case. simp simplifies a + 0 = 0 + a to true using known lemmas.| succ n ih => rw [...] — the step case. rw rewrites the goal along lemmas you name (Nat.add_succ, then the hypothesis ih, then Nat.succ_add) until the two sides are syntactically identical.And then the magic: if it compiles, it's true. No reviewer fatigue. No "the rest is routine." No margin too small to contain the proof. The compiler walks the whole chain and either accepts a genuine value of the theorem's type or refuses. Euclid demanded that every step be earned; Lean enforces it mechanically, two thousand three hundred years later.
That was machines checking proofs. The other direction is stranger: machines proposing them. In 2021 DeepMind worked with knot theorists Marc Lackenby and András Juhász. They trained a neural network on tables of knots and asked it to predict an invariant called the signature from geometric data. The network succeeded — and the way it succeeded flagged an unexpected link between two quantities nobody had connected. The humans chased the hint and proved a brand-new theorem. The net didn't prove anything; it pointed.
It keeps happening. In 2022 a machine-learning classifier did suspiciously well at sorting elliptic curves by rank, and when researchers asked why, they found eerie wave patterns in the average of curve statistics — now called murmurations, after the swirling clouds of starlings. Nobody had predicted them. They're a research area now. AlphaProof reached IMO silver-medal level on olympiad problems. AlphaEvolve (2025) improved a matrix-multiplication record that had stood since Strassen broke it in 1969.
The pattern is consistent and, frankly, reassuring: machine proposes, human disposes. The network finds the wave; the human decides it's worth a definition, formalizes the statement, and proves it. Taste — knowing which pattern is a theorem and which is a coincidence — is still ours. Below is an honest toy showing what a murmuration looks like.
If a compiler checks the proof and a network proposes the conjecture, what's left for us? Three things, and they're the good parts.
Choosing what's worth proving. There are infinitely many true statements; almost all are boring. Deciding which theorem matters — which one opens a door — is an act of judgment no step-counter performs.
The art of the right definition. Here's the book's quietest theme, finally said out loud: most of the great leaps weren't clever proofs, they were the right definition. Euclid's five postulates. Descartes nailing curves to a grid. Cantor pairing the rationals to count them. Shannon deciding information was a bit. Each one was a definition victory — someone choosing the frame, after which the theorems were almost forced. A machine can search a space; a human decides which space is worth searching.
Aesthetics as a search heuristic. Mathematicians chase proofs that are beautiful — short, surprising, inevitable — and beauty turns out to be a reliable signal that you've found the real structure. That instinct is the compass. The machine can walk fast; we still point.
Step all the way back. Thirteen chapters, one question asked over and over with a bigger toolbox each time: recipes that worked but nobody could justify, until the Greeks invented proof (ch.1); then a language of symbols for the unknown (ch.2); the mathematics of change and chance (ch.3); the long campaign to make infinity behave with rigor (ch.4); the discovery that there are many geometries, not one (ch.5); the deep structure of symmetry, truth, and the infinite (ch.6); the logical crisis that, by accident, built the computer (ch.7); information reduced to bits (ch.8); the great abstraction that saw the same skeleton everywhere (ch.9); the wild shapes at the frontier (ch.10); the realization that randomness has a shape (ch.11); the geometry hidden in data (ch.12); and finally, proof itself learning to compile (ch.13). Every era answered the same question — how do you know? — and handed the next era a sharper way to answer it.
Euclid would not understand your terminal. He would absolutely understand what it's checking.