Definition 4.1Finite terminating impartial games under normal play
External cited result A published result used as background or input; not proved in Lean here.
1 Paper text
Definition 4.1 (Impartial game) A finite terminating impartial game is a pair where is a nonempty set of positions and is the (finite) set of legal moves from , with the property that the move relation does not depend on which player is to play (symmetry). We assume the move relation is acyclic and play terminates. We use the last-move-wins convention, usually called normal play: a player with no legal move loses.
Generated from paper_jmlr.tex, lines 406–409.
2 Explain this
The phrase “shared pieces” is a useful board-game intuition. The precise condition is that the same position permits the same moves for either player; it also covers games without physical pieces. In partisan games the available moves can depend on the player's identity.
An impartial game is one in which both players have the same moves from every position (unlike chess, where each player moves their own pieces). "Finite terminating" means play always ends; under normal play the player who makes the last move wins.
Example: NIM is impartial, since any player may reduce any heap.
3 How this is formalised
General impartial games and Sprague–Grundy theory are classical background (Berlekamp, Conway and Guy). The Lean development formalises NIM itself, not general impartial games; its normal-play semantics are in Definition 4.2 and Theorem 4.4.
| Paper anchor | def:impartial (manuscript label) |
|---|---|
| Displayed as | Definition 4.1 |
| Claim | Finite terminating impartial games under normal play |
| Coverage category | External cited result |
| Statement source | paper_jmlr.tex lines 406–409; SHA-256 of the normalised block source f5e8a5a354d70532… |
| Audited correspondence rows | def:impartial |
| Explanations | explain/def:impartial, formal/def:impartial |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is a published classical result. It is cited, not proved in this Lean development.
Build evidence: fresh isolated rebuild of all 38 bundled modules with Lean (version 4.26.0, started 2026-10-10T15:21:56Z, finished 2026-10-10T15:27:00Z: 38/38 modules compiled, 1588 axiom reports, no errors. See Build for the commands and the independent audit of 2026-10-10 (dated evidence).