Section 8.3, paragraph 3Evaluate unseen sizes and positions with explicit computation budgets and solver baselines
Informal interpretation Motivation, interpretation or scope; not a formal claim.
1 Paper text
These are proposed learning challenges, not consequences of the present lower bound. An unresolved structural question is not itself a complexity lower bound, and worst-case hardness need not make a chosen instance distribution difficult. A useful evaluation would reserve unseen sizes and positions, report both training and decision-time computation, and compare play with exact solvers where feasible and strong search baselines elsewhere. Beyond the range of exact verification, improved win rates are evidence of stronger play rather than a solution of an open mathematical problem. The central question is whether self-play discovers reusable strategic structure that extends the range of positions it can handle under a fixed computation budget.
Generated from paper_jmlr.tex, lines 1247–1247.
2 Explain this
Use exact solvers to measure move quality where possible. On larger instances, compare against strong search opponents under stated budgets, while keeping the claim proportional to the evidence: higher win rates show stronger play, not optimal play against every opponent. Generalisation beyond training sizes is central to the proposed tests.
3 How this is formalised
An evaluation proposal, not a mathematical consequence of the AC0 lower bound. No experiment on these harder games is reported here, and no generalisation guarantee is formalised.
| Paper anchor | sec:othergames-p3 (website anchor; the manuscript has no label here) |
|---|---|
| Displayed as | Section 8.3, paragraph 3 |
| Claim | Evaluate unseen sizes and positions with explicit computation budgets and solver baselines |
| Coverage category | Informal interpretation |
| Statement source | paper_jmlr.tex lines 1247–1247; SHA-256 of the normalised block source 813c3e1ba321f205… |
| Depends on | Section 8.3, list |
| Explanations | explain/c-benchmark-evaluation, formal/c-benchmark-evaluation |
| 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).