∑math20

Combinatorics · Result 187

Snaky in 21 Maker moves

1 paperLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Snaky in 21 Maker moves

Snaky in 21 Maker moves

OpenAI · September 25, 2026

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.

Read PDF Download Source

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}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

In the Snaky Maker–Breaker game, the players alternately claim cells of \(\mathbb Z^2\), and Maker seeks a translated, rotated, or reflected copy of the six-cell Snaky shape. The formalization gives a legal strategy that wins within \(21\) actual Maker moves against every legal Breaker play from the empty infinite board. The selected theorem checks disjointness and the move counts throughout play; it does not impose the paper's smaller finite-board restriction.

The linked supplements reconstruct the older \(35\)-move appendix's finite recursive certificate and prove four conditional winning templates from partial positions, assuming the required Maker cells are present and Breaker avoids the corresponding finite envelope.

Comparator links

ResultComparator statement
Reconstruction of the 35-move Snaky certificateSnakyCertificate.lean
Conditional winning templates from finite partial positionsSnakyConditional.lean
Legal Snaky winning strategy within 21 Maker movesSnakyTwentyOne.lean

Scope note on GitHub →