oai-math-revised beta

Browse › Combinatorics › 187 Snaky in 21 Maker moves

Snaky in 21 Maker moves

OpenAI · September 25, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

We prove that Maker can achieve the Snaky hexomino within 21 actual Maker moves against arbitrary legal Breaker play on the initially empty infinite square board. The same bound holds on a $17\times17$ square; in fact, Maker can confine its claims to a fixed 251-cell board.

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-23) and not checked by a person. May be wrong or incomplete. Report an error.

Follow-up works

  • Nándor Sieben, Snaky: Proof sequence for Snaky (GitHub repository, 2026). Gives proof sequences (files proof-sequence-18/19/20.html.gz) in the sense of Sieben's proof-tree paper; the README says they are based on strategies described in this paper, and the 20-move sequence was later formalized in the gotrevor project.
  • Trevor Morris (gotrevor), snaky-15x15: Snaky is a first-player win on 15x15 (GitHub Lean development, October 2026). Reports kernel-checked theorems Snaky.snaky_wins_15x15 and Snaky.snaky_wins_17x17_in_20 and a Breaker win on 9×9, narrowing the smallest winning square-board size to between 10 and 15 after the paper's 17×17 bound. [AI-generated per source]

Comments and discussion

Formalization

  • OpenAI math release, Lean scope notes for result 187 (lean/docs/187.md, 2026). The release's own Lean development: a legal Maker strategy that wins within 21 Maker moves on the empty infinite board (excluding the finite-board restriction), plus reconstructions of the 35-move certificate and four conditional templates.
  • Trevor Morris (gotrevor), Snaky: Maker wins on 17×17 within 20 moves (GitHub formalization notes, 2026). Explains the conversion of Sieben's 1,510 situations into 1,738 cards and the kernel check of snaky_wins_17x17_in_20 (no native_decide), describing it as a refinement of this paper's strategy rather than an optimality result. [AI-generated per source]

Possibly relevant literature (found by the agent, not checked)

Digests and expositions

  • ian52n, snaky-21-move-cards (GitHub repository, 2026). An interactive viewer for the 728 cards of this paper's 21-move certificate, with a Breaker-reply simulator; it rechecks all cards on each load.
  • KaiaSage, snaky-demo (GitHub repository, 2026). An interactive game that implements this paper's Maker strategy from its Appendix D certificate; it also includes a "Snaky in 20" variant, which the README calls an unreviewed draft. [AI-generated per source]
  • heyprof, Snaky in 21 moves (interactive exposition, undated). Presents a playable Maker–Breaker demonstration described as following the paper's embedded proof certificate, with displays for threats, protected regions and the remaining move allowance.
  • OpenAI Math Digest, Snaky in 21 Maker moves (Japanese exposition, 2026-10-15 reference edition). Explains the combination lemma, finite certificate, legal policy and finite-board corollary, and reports rerunning two author-supplied Python reconstruction programs while excluding Lean compilation from its checks. [AI-generated per source]

News and blogs

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:Snaky-in-21-Maker-moves-September-25-2026,
  author = {{OpenAI}},
  title = {{Snaky in 21 Maker moves}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Snaky-in-21-Maker-moves-September-25-2026/article.pdf}{OAI:Snaky-in-21-Maker-moves-September-25-2026}},
  year = {2026}
}

From OpenAI's README for this paper:

Verification

The verification programs require Python 3.10 or later and only the standard library. To run the short 21-move certificate checker and the reconstruction suites for all three certificates from the paper directory, use a new output directory:

python3 -B verification/verify_certificate.py
python3 -B verification/supporting/verify_all.py --output-dir ../snaky-verification-output

Successful execution prints PASS; the second command also writes a report.json with status PASS in the requested output directory. These are finite certificate-reconstruction checks, not an executable playing policy or a replacement for the paper's proofs.

Lean formalization

OpenAI provides Lean files for this family: lean/docs/187.md. The Lean statements have not been checked by people against the paper's claims.

Family 187: Snaky in 21 Maker moves

Settles the Snaky achievement problem: Maker can force the six-cell Snaky shape within 21 of its own moves on the initially empty infinite square board. Maker moves first, each player claims one free cell per turn, and translations, rotations and reflections count as wins.

This is the only paper in this family.