Snaky in 21 Maker Moves: How OpenAI’s Proof Ended a 47-Year Tic-Tac-Toe Mystery

Six squares were enough to leave a gap in a decades-old classification of tic-tac-toe variants. The shape was Snaky: a straight four-cell body with a two-cell kink. OpenAI’s September 25, 2026 paper, Snaky in 21 Maker Moves, supplies a guaranteed winning strategy from an empty board against every legal defensive response.

Maker can finish within 21 of its own claims, on the infinite square grid or a finite 17×17 board. The mechanism is a reusable rule for combining conditional wins, backed by an exact certificate. This is a concrete strategy theorem, a different kind of evidence from the scores discussed in our LLM mathematics benchmark guide.

1. What OpenAI’s Snaky in 21 Maker Moves Proof Actually Establishes

Theorem 1 fixes one legal Maker policy before Breaker chooses any responses. That policy completes a permitted Snaky copy within at most 21 actual Maker claims, including replacement moves when a planned cell is already owned. Maker starts, so victory occurs no later than individual turn 41, after at most 20 Breaker replies.

1.1. Snaky Proof: Key Facts

“At most” matters. As in our explanation of bounds in the Hadwiger–Nelson problem, establishing a bound does not identify the exact answer. Snaky might admit a faster guaranteed win.

2. The Original Snaky Problem: Six Squares, Two Players, One Elusive Win

A hexomino is six unit squares joined edge to edge. Index cells by integer coordinates. Snaky’s body occupies $(0,0)$, $(1,0)$, $(2,0)$ and $(3,0)$, with the remaining cells at $(3,1)$ and $(4,1)$. Call this six-cell set $S$.

An allowed target is $t+R(S)$: an integer translation $t$ after one of eight square symmetries $R$. Quarter turns and reflections count. Scaling does not. Permitted motions are part of the theorem, just as translation-only rules matter in periodic tiling.

In the Snaky Maker-Breaker game, players alternately claim unoccupied cells, with permanent ownership. Only Maker seeks the target. Breaker merely obstructs it. Maker may own extra cells. Ordinary tic-tac-toe gives both players a winning objective, so its familiar intuition needs adjustment.

3. Why Snaky Remained Unsolved for 47 Years

The 47-year framing counts from the game’s 1979 public presentation in Martin Gardner’s column. A 1996 mathematical discussion preserved by David Eppstein records both that reference and the continuing uncertainty.

Snaky was the exceptional unresolved hexomino in the planar weak-game classification. Other six-cell targets had defensive classifications, while Snaky resisted the standard pairing approach. Its small size made the question easy to state, not easy to search.

A promising attack was insufficient. Breaker could choose an unexpected nearby block or play arbitrarily far away. A proof needed one strategy covering every legal reply, without quietly granting Maker extra opening stones.

4. The Previous Barrier: Pairing Strategies, Handicaps and Higher Dimensions

A pairing defense divides relevant cells into disjoint pairs. Whenever Maker takes one member, Breaker takes its mate. If every target contains a complete pair, Maker cannot finish. Proving that no such defense exists only eliminates this defensive family. Breaker might still win another way.

Earlier work established a 41-dimensional win. Halupczok and Schlage-Puchta’s 2007 paper, Achieving Snaky, reduced that to three dimensions, proved defeat on an 8×8 board, and established a planar handicap-one win. Here one handicap lets Maker place two stones before Breaker’s first reply. Ito and Miyagawa also supplied a handicap-one construction.

Those results changed either the space available or the opening rules. The 2026 proof handles two dimensions, an initially empty board, and ordinary alternating claims. That is the missing combination of conditions.

5. The Tactical Breakthrough: Four-in-a-Row Threats and Winning Forks

Four consecutive Maker cells form Snaky’s body. Add the right perpendicular cell and another cell becomes an immediate winning completion. Breaker must occupy that completion or lose on the next Maker move.

A five-cell line is more dangerous. Near an endpoint, take a clean three-cell strip in the neighboring row. “Clean” means Breaker owns none of it. Claiming its middle creates two alternative Snaky completions, using different four-cell subrows of the five. Breaker can occupy only one completion. The other wins.

Proposition 7 gives a precise local guarantee. At Maker’s turn, suppose Maker owns the row from $(0,0)$ through $(3,0)$ and Breaker owns at most three cells in the integer rectangle $Q=[-3,6]\times[-4,4]$. Then Maker has already won or can force a win. Extra Maker cells and arbitrary Breaker cells outside that rectangle are allowed.

The three-blocker hypothesis is essential to that statement. The proposition explains useful tactics, but the 21-move theorem does not assume play ever reaches this sparse neighborhood. Its certificate supplies the full argument.

6. Conditional Winning Positions: The Mathematics Behind A, T and h

The proof packages a sufficient condition as a triple $(A,T,h)$. The required set $A$ lists cells Maker must already own. The finite envelope $T$ must contain no Breaker cells, and includes $A$. Height $h$ bounds the number of additional actual Maker claims needed.

Write $M$ and $B$ for current Maker and Breaker ownership. A valid triple applies at every Maker turn satisfying $A\subseteq M$ and $B\cap T=\varnothing$, with the ownership sets finite and disjoint. It promises either an existing target or a win within the stated budget.

The envelope need not be empty. Some of its cells can already belong to Maker. Breaker can own any finite collection outside it. Nor must the position have arisen through a particular sequence. Those freedoms make the conditions reusable.

Think of a card as a function with explicit preconditions. Extra Maker ownership cannot spoil the promise, while old Breaker ownership is excluded exactly where the continuation needs protection. Translating, rotating or reflecting both sets transports the same guarantee without changing its height.

7. The Combination Lemma: Why Breaker Cannot Block Every Continuation

Lemma 3 combines a finite, nonempty family of valid child cards $(A_i,T_i,h_i)$ at a chosen pivot $p$. Its parent is defined by three recurrences:

The union symbol collects cells appearing in any child. The intersection collects cells shared by every child envelope. The set difference removes the pivot from the parent’s ownership requirement.

Maker first claims the pivot. Every required child cell is now Maker-owned, because their union was required except possibly at that pivot. Crucially, Maker also owns the entire intersection of the child envelopes. This is stronger than merely preparing several attractive attacks.

Breaker’s next legal claim cannot lie in that intersection: those cells are occupied by Maker. Therefore at least one child envelope misses the new Breaker cell. Every older Breaker cell also misses it, because each child envelope lies inside the parent envelope. That child’s complete preconditions survive.

For a simple two-child example, suppose their envelopes share only cells Maker now owns. A legal Breaker reply may enter the first envelope, the second, or neither, but cannot enter both. Choose the untouched continuation. The full rule permits many children and larger intersections, provided the parent requires ownership of every shared cell apart from the pivot.

A remote reply is covered automatically. Outside the parent envelope, it misses every child. The recurrence charges one move for the parent and the largest child budget, so height induction supplies the bound.

If Maker already owns the pivot, claiming it again would be illegal. Maker instead claims any genuinely free cell, spends one actual move, and allows Breaker a real reply. Ownership of the intersection still holds. Counting this replacement prevents the proof from obtaining a free turn. A separate Breaker-turn version saves that parent move only when its ownership conditions already hold before Breaker plays.

8. Inside the 728-Card Proof Certificate: From Six Bases to the Final Empty Requirement

The six base cards each require five cells of one Snaky and protect the whole target. The sixth cell is either already Maker-owned or free to complete the shape. Each base therefore has height one.

Card 6 illustrates composition. Its requirement is the vertical five $(0,0)$ through $(0,4)$. Its envelope adds $(1,3)$, $(1,4)$ and $(1,5)$. The pivot $(1,4)$ prepares two completions, so height two suffices. Card 7 combines two placements of card 6. Its required column shrinks to $(0,1)$ through $(0,4)$, with pivot $(0,5)$ and height three.

The remaining numbered cards reuse earlier cards under integer translations and square symmetries. Nested, unnumbered combinations also occur. Thus 728 numbered cards is not the entire node count: the certificate includes 898 inline combinations. Backward references make the construction acyclic and permit induction.

The final card, 727, combines 32 placed children. Every placed required set is exactly the pivot $(8,8)$. The cumulative envelope intersection contracts as follows.

8.1. How Card 727 Removes Every Extra Shared Cell

The last column counts common envelope cells other than the pivot after that group and all preceding groups. At the end, only the pivot remains shared. The recurrence removes it, leaving $A=\varnothing$. Reconstruction gives a 251-cell envelope and height 21.

This certificate is an auditable output, rather than a record of every discovery attempt. The distinction between finding constructions and checking them also matters in AI-assisted mathematical search. Here the published certificate is sufficient for reconstruction without rerunning a strategy search.

9. How the Proof Produces One Guaranteed Strategy Against Every Breaker Move

A collection of conditional wins still needs an executable choice rule. Start with card 727. Its empty requirement holds before the first move, and its envelope contains no Breaker cells. Maker takes the pivot $(8,8)$.

Fix a cell enumeration and every child-list order before play. At each subsequent combination, take the placed pivot if free, otherwise the first free replacement. After Breaker replies, select the first child whose envelope avoids that reply. The lemma guarantees that one exists and that its other preconditions remain satisfied.

Carry forward the child’s translated or reflected coordinate frame. At a base, claim the missing target cell unless Maker has already won. Every nonterminal descent spends one Maker claim and strictly decreases height. Starting at 21 therefore guarantees termination within 21 claims.

For histories inconsistent with earlier prescribed choices, the policy selects a fresh cell by the same enumeration. This fallback makes it globally legal. On histories reached by following the strategy, the certificate invariant supplies the winning guarantee.

The order of commitments matters: one policy works against every legal Breaker continuation. Maker does not inspect future replies. This is a stronger guarantee than successful sampled play or a generate-and-critique research workflow.

10. From the Infinite Grid to 17×17: What the 21-, 25- and 35-Move Proofs Establish

Every child envelope nests inside its parent. All prescribed pivots and base targets consequently stay within the final 251-cell envelope, itself contained in the 17×17 square. A replacement stays there too: before Maker claim 21, at most 40 cells are occupied, leaving ample room for a fresh claim. This proves Corollary 6.

10.1. Three Constructions With Different Information

The 25-move route uses required cells as placement anchors. The 35-move route handles unbounded distant replies through omitted regions and nearby replies through a two-stone opening obtained on separate turns. Its local cards have height at most 34, with opening costs included in the 35-claim total.

These are distinct sufficient constructions. Their bounds do not establish optimal play, minimal board size or practical execution speed. As with theoretical factorization guarantees, a mathematical bound answers a specific question about the stated model.

11. Lean Verification, Proof Certificates and the Limits of the Result

There are separate checks here. The combination lemma supplies mathematical soundness. Exact reconstruction establishes the certificate’s finite sets and heights. Independent implementations provide additional checks. A checksum identifies the data bytes, but cannot prove the game-theoretic implication. Reading exact certificates alongside their mathematical bridge also matters in our Laughlin spectral gap analysis.

For this article, the published Python verifier passed, reconstructing 728 cards and confirming the empty requirement, 251-cell envelope and height 21. That run checks the finite reconstruction. It does not independently compile Lean or reproduce every supplied verification program.

The official Snaky Lean proof scope reports a legal 21-claim strategy on the empty infinite board, including disjointness and move counts. It excludes the smaller finite-board restriction. Separate formalizations cover selected older 35-move reconstruction and conditional-template results. The paper’s limited Appendix C supplement and the later infinite-board theorem therefore have different scopes.

Comparator challenge statements can contain an unproved placeholder while the separate Snaky solution module supplies the proof, a distinction explained in our Barnette proof verification guide. Formalization also requires faithful definitions, as our Fermat formalization explainer discusses. Neither a successful Python run nor a scope note should be described as an independent local Lean replay.

OpenAI’s October 6 mathematics release attributes the collection to an internal frontier model. This result demonstrates a certified strategy, not a measured general-purpose game-playing capability. It leaves the strong game, exact minimum move count and smallest winning board unresolved by this proof.

Snaky in 21 Maker Moves rewards reading the conditions as carefully as the conclusion. Follow Binary Verse AI’s AI mathematical proof coverage for more explanations that connect headline results to the mechanisms and verification they actually provide.