OpenAI claim summary for Math-2623
mathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
The claimed winning policy applies to the exact six-cell target, translation/rotation/reflection conventions and unbiased Maker-first empty infinite-lattice game in the question. Winning within twenty-one Maker claims is stronger than the existence of an unrestricted finite winning strategy.
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
Maker winning strategy for Snaky on the infinite square lattice
OpenAI's claim
Snaky within 21 Maker claims: The paper claims a Maker strategy for Snaky using at most 21 Maker moves against every legal Breaker response. It can operate on a fixed 251-cell region inside a $17\times17$ square.Mathematical statement of the claimed result
Mathematical claim 1.
On the initially empty board $\mathbb Z^2$, Maker moves first and each player then claims one unowned cell per turn. For \[S=\{(0,0),(1,0),(2,0),(3,0),(3,1),(4,1)\},\] targets are $t+RS$ with $t\in\mathbb Z^2$ and $R$ a signed permutation matrix, so rotations and reflections but no scaling are allowed. The claim supplies one globally legal Maker policy which, against every legal Breaker continuation, owns an entire target within at most $21$ Maker claims. It therefore asserts a winning strategy for the ordinary unbiased Snaky game.Outline of the argument
Snaky within 21 Maker claims: Finite winning conditions list required Maker cells, a Breaker-free envelope, and a bound on remaining moves. Backward references combine child conditions after one chosen Maker claim, using envelope intersections to ensure that one Breaker move cannot kill every continuation. A 728-condition certificate closes at the empty initial position; induction extracts a legal policy with the stated move bound.Formal verification
Family 187 describes Lean coverage for the infinite-board 21-move policy and older conditional certificates; the smaller-board restriction is not selected.Snaky within 21 Maker claims: The manuscript links SnakyCertificate.lean, SnakyConditional.lean, SnakyTwentyOne.lean.
The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.
This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.
Status caveat
OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.Sources
- OpenAI, Snaky in 21 Maker moves, 2026-09-25; citation key
OAI:Snaky-in-21-Maker-moves-September-25-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main. - Family 187: Lean scope.
- Comparator SnakyCertificate.json.
- Comparator SnakyCertificate.lean.
- Comparator SnakyConditional.json.
- Comparator SnakyConditional.lean.
- Comparator SnakyTwentyOne.json.
- Comparator SnakyTwentyOne.lean.
- OpenAI catalogue entry.