The Snaky achievement game
From OpenAI Aftermath
The Snaky achievement game is the Maker–Breaker game in which two players alternately claim cells of the square grid and Maker tries to own a copy of the six-cell polyomino called Snaky, in any position, rotation or reflection. Whether Maker wins on the empty plane was the one hexomino case left open in Harary's polyomino achievement games. A manuscript dated 25 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims that Maker wins within 21 moves. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- Sieben attributes polyomino achievement games to Frank Harary. His account records handicap-two strategies of Harary, Harborth and Seemann and the nonexistence of a pairing defense for Snaky, which Csernenszky, Martin and Pluhár later proved without a computer.
- Halupczok and Schlage-Puchta proved that Snaky wins in three dimensions, loses on an 8 × 8 board, and wins in the plane with one extra Maker stone at the start; Ito and Miyagawa also gave a construction with that handicap. Sieben gave a finite proof sequence for the handicap and described the ordinary planar problem as undecided.
The original result
- Claim. Theorem 1 of the manuscript states that on the initially empty infinite square board, with Maker moving first and no handicap, one legal Maker strategy completes a copy of Snaky within at most 21 of Maker's own claims against every legal play of Breaker. The abstract adds that the same bound holds on a 17 × 17 board, and that Maker can keep its claims inside a fixed board of 251 cells. The manuscript does not assert optimal move counts or board sizes, or a result for the strong game.
- Method, as described: a finite certificate of strategy cards, each pairing required Maker cells with an envelope that Breaker must avoid, combined by a recursive rule. Independent 25-move and 35-move constructions are given as well.
- Source. At commit
1581d4c: Snaky in 21 Maker moves. - Formalization, as described by the repository. The scope note lean/docs/187.md states that the Lean formalization gives a legal strategy that wins within 21 actual Maker moves from the empty infinite board, and that it does not impose the smaller finite-board restriction. Supplements reconstruct the earlier 35-move certificate and prove four conditional winning templates. The Comparator challenges are
SnakyTwentyOne,SnakyCertificateandSnakyConditional.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 23 October 2026) |
|---|---|---|---|---|
2026-10-07 (latest commit b18ed32, 12 October 2026) |
T. Morris, gotrevor/snaky-15x15 (GitHub) | Extension (finite boards) | States that Maker wins on the empty 15 × 15 board, the board size in Harary's conjecture as cited there, by a strategy certificate checked by an independent checker and by a Lean theorem, Snaky.snaky_wins_15x15, whose card checker is proved sound and run in the kernel. The repository also checks Sieben's 20-move sequence on 17 × 17 in Lean, and reports a Breaker win on 9 × 9 by a certificate with an independent checker, so that the smallest square board on which Maker wins lies between 10 and 15 according to its notes. The notes state that the search, the certificate and the text were produced by Claude at the author's direction. |
GitHub repository, with an online game against the proved strategy. |
2026-10-08 (latest commit da8236f, 16 October 2026) |
N. Sieben, nandorsieben/snaky (GitHub) | Extension (fewer moves) | Contains files titled 18-move, 19-move and 20-move Snaky proof sequences. The README states that they are based on the strategies of the manuscript, and refers to an earlier volume of Integers for the definition of a proof sequence. | GitHub repository; the 20-move sequence is checked in Lean in Morris's repository. |
2026-10-08 (latest commit 75e03ff) |
KaiaSage/snaky-demo (GitHub) | Use (demonstration) | A browser demonstration of the manuscript's Maker strategy on a 19 × 19 board. | GitHub repository. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit bb5fdb6, 18 October 2026) |
Review (fidelity of the formal statements) | Rates this family "full" and records sandboxed Comparator passes for SnakyTwentyOne, SnakyCertificate and SnakyConditional. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
2026-10-09 (commit 239dae4) |
erebos-labs/snaky-bounded-lean (GitHub) | Verification (Lean soundness for the 20-move strategy) | Lean proofs that a bounded Snaky strategy given by accepted cards wins on the infinite plane, described as a verification contribution for Sieben's strategy using Morris's generic checker. The certificate needed for the unconditional 20-move theorem is not included, and the README makes no claim of a new strategy or bound. | GitHub repository. |
| 2026-10-10 | cert-machine, openai/math lane K: runs 38019899278 for SnakyTwentyOne and SnakyConditional, and 38051470892 for SnakyCertificate | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept all three solutions, in 2,176 s, 2,195 s and 1,308 s. | Repository. |
2026-10-15 to 2026-10-16 (commit bc1a918) |
S. van de Kamp, shjvandekamp/math, topics/snaky (GitHub) | Extension (fewer moves) | States that Maker wins within 19 of its own moves on the empty infinite board and on 17 × 17, combining Sieben's 20-move strategy with local tactics from Morris's 15 × 15 work, and within 24 moves on 15 × 15, improving the bound of 25 of Morris's certificate. Both bounds are given with certificates and Lean theorems. | GitHub repository; the notes describe the bounds as AI-assisted contributions offered for public scrutiny, with no optimality claim. |
| 2026-10-16 | J. Jardine, Lattice24, referee review rank_435 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995) | Review (AI-assisted audit) | Reports no gap. It rebuilt evaluators for the 21-move and 35-move certificates and checked the 25-move lemma by hand. Its one minor note concerns packaging: the verification script stops on file-permission checks in a fresh checkout, and passes after the permissions are restored. | Review record. |
2026-10-17 (commit 252b494) |
ian52n/snaky-21-move-cards (GitHub) | Use (interactive viewer) | An interactive viewer of the 728 cards of the 21-move certificate with a simulator of Breaker replies. On every load the page recomputes the cards, checks that each of the 37,042 classes of Breaker replies leaves a child card alive, and compares the certificate's checksum with the manuscript. | GitHub repository and web page. |
2026-10-19 (latest commit 85e9cc3, 21 October 2026) |
maverick0351a/finite-congruence-checks (GitHub) | Use (formal restatement) | Among checks of several results of the collection, records a Lean statement that Maker has a strategy within 21 fresh claims on the manuscript's 251-cell board and on the containing 17 × 17 square, and an independent reconstruction of the 728-card certificate. The repository states that it makes no claim of a new mathematical theorem. | GitHub repository. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
