NIM paper · interactive edition Interactive edition · paper, explanations and Lean proofs.

Section 8.3, listSprouts, Chomp and Grundy's game offer distinct proposed self-play challenges

Informal interpretation Motivation, interpretation or scope; not a formal claim.

1 Paper text

  • Sprouts. Players join spots by noncrossing curves, add a spot on each new curve, and keep every spot’s degree at most three. The normal-play outcome conjecture for the standard nn-spot opening remains open despite substantial progress with exact solvers (Čížek et al., 2026). Learning to exploit the evolving region structure, and to choose winning moves in intermediate positions, would be a stronger test than predicting opening outcomes from nn alone.

  • Chomp. A move removes a chosen square and all squares above and to its right; taking the distinguished corner loses. Strategy stealing establishes a first-player win on every nontrivial rectangle, but does not supply the winning moves (Berlekamp et al., 2001–2004). Larger boards and their irregular intermediate positions offer a challenge beyond solved special families; the analysis of Chomp continues to pose open problems (Nowakowski, 2025). The benchmark should test move selection and generalisation across shapes, not just the known opening winner.

  • Grundy’s game. A move splits one heap into two nonempty unequal heaps. Whether its nim-value sequence is eventually periodic remains an open problem (Nowakowski, 2025). This offers a test of whether self-play discovers useful structure in component values and how they combine. Testing unseen heap sizes and sums of heaps can distinguish such progress from memorising a finite table.

Generated from paper_jmlr.tex, lines 1241–1245.

2 Explain this

The proposed games test different kinds of structure. Sprouts involves evolving planar regions; Chomp involves board shape and move choice even when an opening winner is known; Grundy's game involves learning component values and combining them. These are proposals for future evaluations, not games solved by the present paper.

The game names alone do not define a benchmark. The starting-position distribution, allowed information, training sizes, held-out sizes and search budget must all be specified. An agent that predicts a familiar opening pattern may still fail to choose a winning move in a new intermediate position.

3 How this is formalised

No new Lean theorem is asserted. The paper cites the published Sprouts solver study and the open-problems literature; the learning challenges are the author's proposed applications. The existing NIM formalisation does not certify these games' rules, outcome conjectures, strategies or learnability.

Coverage record
Paper anchorsec:othergames-list1 (website anchor; the manuscript has no label here)
Displayed asSection 8.3, list
ClaimSprouts, Chomp and Grundy's game offer distinct proposed self-play challenges
Coverage categoryInformal interpretation
Statement sourcepaper_jmlr.tex lines 1241–1245; SHA-256 of the normalised block source 79d3df280f7f68aa…
Prose-to-formal notes

A research proposal supported by cited literature, not a Lean theorem or a new experiment. Open structural questions and known opening outcomes are distinguished from learning winning moves.

Explanationsexplain/c-harder-benchmarks, formal/c-harder-benchmarks
Build evidencefresh 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).