Several heaps of stones. Take as many as you like, from one heap. Last stone wins. There is a perfect way to play — and the whole of it is a single number you compute by counting in binary.
Two people, a few piles of stones. On your turn you pick one pile and remove any number of stones from it — one, a handful, the whole pile — as long as you take at least one. Then your opponent does the same. Whoever takes the very last stone wins. Children invent this game on their own; it is called Nim.
It feels like it should come down to nerve and luck. It does not. Nim is completely solved, and has been since 1901, when a Harvard mathematician named Charles Bouton published the answer. From most starting positions, the player who moves first can force a win — and the recipe for doing so is not a thicket of cases. It is one arithmetic operation, applied to the pile sizes, written in binary.
Play it first. The machine below has the strategy; you do not, yet. See if you can take a stone off it.
Each row is a heap. Click a stone to take it and every stone to its right in that row — that is your move, any amount from one heap. The machine answers instantly. If you start from a position it can win from, it will not lose; if you start from one of the rare positions it is losing, you can beat it — but only by playing perfectly yourself. The panel on the right keeps the only score that matters.
However well you played, one thing kept happening: whenever it was your turn, the bottom row of that binary panel was all zeros. The machine handed it to you that way every single time, and there was nothing you could do to give it back the same. That bottom row is the whole secret.
Write each heap in binary and stack them. Now add up each column — but throw away the carries, so each column is just "an even number of 1s, or an odd number." A column with an odd number of 1s becomes a 1; an even number becomes a 0. The resulting number is the nim-sum: the heaps combined with exclusive-or, ⊕. It is the same XOR your computer does ten billion times a second, and on the stones it means one crisp thing — a column is hot if an odd number of heaps have a stone of that size.
Bouton's theorem: the player to move loses, under perfect play, exactly when the nim-sum is zero.
So the strategy writes itself. If the nim-sum is not zero, you are in a winning position, and there is always a move that makes it zero — hand that to your opponent. If the nim-sum already is zero, you are lost against perfect play; every move you make will light some column up, and a good opponent will douse it again. Below: type any position and watch the move-finder locate the winning move, the way the machine does.
The move-finder never fails on a hot position, and that is not luck — it is forced. Take the highest column that is lit in the nim-sum. Some heap must have a stone in that column (that is what made the column odd). XOR that heap with the nim-sum: its top lit bit flips from 1 to 0, so the number gets strictly smaller — a legal move, you only ever remove stones — and after it, every column is even again. The nim-sum is zero. You have handed your opponent the dead position.
Strip the game down and a perfect strategy needs exactly two guarantees, and the whole of Bouton's theorem is these two:
Progress — from any position with nim-sum ≠ 0 there is a legal move to a position with nim-sum 0. (You can always restore the zero.)
Closure — from any position with nim-sum 0, every legal move leaves nim-sum ≠ 0. (Your opponent can never hand the zero back.)
Add the obvious fact that every move removes at least one stone, so the game must end, and the strategy is airtight: you move to zero (Progress); your opponent is forced off zero (Closure); the stone-count falls every turn, so the heaps must eventually empty — and the empty table has nim-sum zero, reached the instant after one of your moves. Your opponent is the one staring at nothing to take.
A program can check this on small games — and one does, below, grinding through every position with a few small heaps by brute-force backward induction and confirming "the player to move loses" lands on exactly the same positions as "nim-sum is zero." But a brute-force sweep, however large, only ever sees finitely many positions. The two facts are claims about all of them: any number of heaps, of any size. To close that gap you do not test — you prove, and you let a machine check the proof.
And then the part no finite check can reach — proved for every position and every heap, machine-checked by Lean 4, zero imports, trusting nothing but the kernel:
-- research/nim/lean/Nim.lean (excerpt — the two load-bearing theorems) theorem progress {xs : List Nat} (h : nimber xs ≠ 0) : ∃ ys, Move xs ys ∧ nimber ys = 0 theorem closure {xs : List Nat} (h0 : nimber xs = 0) (hm : Move xs ys) : nimber ys ≠ 0 -- the only trusted component is Lean's type checker: #print axioms progress ⇒ [propext, Quot.sound] -- no sorry, no choice
That is the thing worth holding onto. The bot winning a thousand games proves nothing — a bot can win a thousand games on a strategy that fails on the thousand-and-first. The exhaustive sweep is better: it is a real proof, but only for the positions it had time to enumerate. What the page rests on, in the end, is neither — it is a proof a machine has read symbol by symbol and certified covers every Nim position there will ever be. The unbeatable machine you played is just the friendly face of that certainty.
Nim is also the seed of something larger. Every impartial game — games where both players have the same moves — turns out to be equivalent to a single Nim heap of some size, its Grundy value; this is the Sprague–Grundy theorem, and it is why the XOR you just watched governs a whole zoo of games beyond stones in rows. Its strange cousin lives one door down: Wythoff's game adds a single move — take the same from both heaps — and its losing positions, instead of falling out of binary, fall along two lines whose slope is the golden ratio. Same family; the arithmetic could not look more different.