Section 1, paragraph 2NIM rules, impartiality and why NIM is central
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
In NIM, two players take turns removing any positive number of tokens from a single heap; the player taking the last token wins. It belongs to the broad class of impartial games: both players have the same legal moves from a given position. Many such board games can be thought of as games with shared pieces, whereas in partisan games, such as chess, legal moves depend on which player is to move. NIM is central to impartial-game theory because every finite terminating impartial position under the last-move-wins convention is equivalent, in sums of games, to a single NIM heap (Section 4).
Generated from paper_jmlr.tex, lines 85–85.
2 Explain this
NIM has heaps of tokens. On each turn, remove at least one token from one heap; taking the last token wins. For example, can become , but a single move cannot alter both the first and second heaps.
Impartial games allow the same moves to either player. Shared pieces are a useful intuition; the formal condition concerns legal moves, not ownership. Chess is partisan because the players move different colours. The striking link to NIM is explained in Section 4.3, paragraph 1: every finite terminating normal-play impartial position can be replaced, in sums, by one NIM heap. This is a structural statement, not an efficient method for solving every impartial game.
3 How this is formalised
This introduction combines the classical impartial-game definition, Definition 4.1, with the NIM rules, Definition 4.2, and the external Sprague–Grundy theorem, Section 4.3, paragraph 1. The Lean development checks NIM, rather than the general Sprague–Grundy theorem.
| Paper anchor | c-intro-games (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 1, paragraph 2 |
| Claim | NIM rules, impartiality and why NIM is central |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 85–85; SHA-256 of the normalised block source 0ec57899a55792f1… |
| Depends on | Definition 4.1, Definition 4.2, Section 4.3, paragraph 1 |
| Explanations | explain/c-intro-games, formal/c-intro-games |
| Build evidence | fresh isolated rebuild, audit report |
4 Lean statement and source
No Lean statement corresponds to this claim. This is interpretation or motivation, not a formal mathematical claim.
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).