Section 3, “Reinforcement learning in combinatorial games”Prior work on RL difficulties in impartial games; the lower bound is about a restricted model
External cited result A published result used as background or input; not proved in Lean here.
1 Paper text
Reinforcement learning in combinatorial games. While RL has mastered domains such as Go and chess, impartial games remain a useful stress test because optimality is governed by exact algebraic invariants rather than approximate pattern matching. Zhou and Riis (Zhou and Riis, 2026, 2023) studied reinforcement-learning difficulties in impartial games. Our lower bound identifies a representational obstruction in a restricted model; determining which mechanisms explain failures in ordinary neural training requires separate experiments.
Generated from paper_jmlr.tex, lines 388–391.
2 Explain this
Impartial games are a stress test for reinforcement learning because optimal play is governed by an exact algebraic invariant rather than by approximate patterns. The paragraph cites the earlier studies by Zhou and Riis and separates two questions: a representational obstruction in a restricted model (this paper) and the mechanisms behind failures of ordinary training (which need separate experiments).
3 How this is formalised
Cited background and a scope remark; nothing here is formalised.
| Paper anchor | par-reinforcement-learning-in-combinatorial-games-p1 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 3, “Reinforcement learning in combinatorial games” |
| Claim | Prior work on RL difficulties in impartial games; the lower bound is about a restricted model |
| Coverage category | External cited result |
| Statement source | paper_jmlr.tex lines 388–391; SHA-256 of the normalised block source 7ec0fd7179c570fe… |
| Explanations | explain/c-rw-rl, formal/c-rw-rl |
| 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).