Nim

Several heaps of objects sit on the table. On your turn you remove any positive number of objects from a single heap — one object, the whole heap, or anything in between. Under the normal play convention modelled here, the player who takes the last object wins. The classic board is three heaps of sizes {3, 4, 5}.

Nim is impartial — both players always have exactly the same moves available from any position — which makes it the foundational example of combinatorial game theory: deterministic, fully observable, finite, and with no chance element anywhere.

Nim is encoded as an explicit transition system: a position is a sorted tuple of heap sizes with empty heaps dropped, a move is “take between 1 and everything from one heap”, and the empty position is terminal — the player to move there has lost, because the previous player took the last object. Sorting the heaps is the game’s natural symmetry reduction: heaps are unordered, so boards differing only in heap order merge into one canonical position, turning the game tree into a directed acyclic graph.

The value of the game collapses to a single number, the nim-sum — the bitwise XOR of the heap sizes. By Sprague–Grundy theory, every position of an impartial game carries a Grundy value (a number computed recursively from its successors), a position is a loss for the player to move exactly when that value is 0, and the value of a sum of independent games is the XOR of the parts. Since a single heap of size n has Grundy value n, Nim’s Grundy value is the nim-sum — giving Bouton’s theorem (1901): the first player wins iff the nim-sum is non-zero.

That closed form is established three independent ways. First, a brute-force backward-induction game-tree solver that never looks at the nim-sum confirms, on every configuration with at most 3 heaps of size at most 6 (400 positions), that the Grundy value equals the XOR and that XOR = 0 exactly characterises the losing positions. Second, the two invariant lemmas that constitute Bouton’s winning strategy are discharged by the z3 SMT solver — an automated theorem prover — as for-all theorems over all positions of a heap layout, using bit-vector XOR and proving each by the unsatisfiability of its negation: L1 (progress), from any position with nim-sum ≠ 0 there exists a move to nim-sum 0; and L2 (closure), from nim-sum 0 every move yields nim-sum ≠ 0. Third, the strategy is extracted, not just asserted: from nim-sum S ≠ 0, reduce a heap h with h ⊕ S < h to h ⊕ S, and tests verify the returned move always lands on nim-sum 0 and leaves the opponent in a position the independent solver confirms is lost.

Nim is exactly solved — every figure is exact, none estimated. The losing positions for the player to move are precisely those with nim-sum 0; the whole game collapses to one number. On the classic board {3, 4, 5} the nim-sum is 3 ⊕ 4 ⊕ 5 = 2 ≠ 0, so the first player wins; a winning move is to reduce the heap of 3 to 1, giving {1, 4, 5} with nim-sum 0. Sample verdicts:

A bot that plays the L1 move is unbeatable from any winning position: it moves to nim-sum 0, the opponent is forced back to nim-sum ≠ 0 by L2, and heaps strictly shrink until the bot takes the last object. From a nim-sum-0 start the mover is theoretically lost against perfect play — the certificate is “first player wins iff nim-sum ≠ 0”, not “the bot always wins”. Misère Nim (last to move loses) is a different game and intentionally out of scope.

Browse the other verified board games.