Section 8.3, paragraph 1Some impartial games (Geography) have PSPACE-complete winner problems
External cited result A published result used as background or input; not proved in Lean here.
1 Paper text
By Sprague–Grundy theory, every finite impartial game position has a nimber. However, the computational complexity of determining nimbers varies widely. Some impartial games have PSPACE-complete winner problems, such as directed vertex Geography (Schaefer, 1978). Unless , no polynomial-time algorithm solves all such instances. Having a nimber does not supply an efficient way to compute it.
Generated from paper_jmlr.tex, lines 1237–1237.
2 Explain this
Every finite impartial game position has a nimber, but computing it can be very hard. For directed vertex Geography the winner problem is PSPACE-complete (Schaefer, 1978); unless P = PSPACE, no polynomial-time algorithm solves all instances. Existence of a nimber gives no efficient way to compute it.
3 How this is formalised
A classical external result, cited; not formalised.
| Paper anchor | sec:othergames-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 8.3, paragraph 1 |
| Claim | Some impartial games (Geography) have PSPACE-complete winner problems |
| Coverage category | External cited result |
| Statement source | paper_jmlr.tex lines 1237–1237; SHA-256 of the normalised block source c1573656b15b22b2… |
| Explanations | explain/c-geography, formal/c-geography |
| 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).