Snaky and a 21-move certificate

Source and verification

This article explains family 187 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

🏷️ The Snaky game

Snaky is the six-cell polyomino

$$\begin{array}{rl}S=\{& (0,0),(1,0),(2,0),\\ & (3,0),(3,1),(4,1)\}\subset {\mathbb{Z}}^2.\end{array}$$

The board is the entire square lattice. Maker moves first; then Maker and Breaker alternate, each claiming one previously unclaimed cell. Maker wins by owning an integral translation, quarter-turn rotation, or reflection of $S$. Scaling is not allowed. Breaker merely tries to prevent this; Breaker does not need to build a competing shape.

Manuscript claim

From the empty board, one globally legal Maker strategy wins against every legal Breaker continuation within 21 actual Maker claims, hence by the 41st individual turn. The paper also obtains the same bound on a $17\times 17$ board. Neither move count nor board size is claimed optimal. (OpenAI, 2026)

There are no handicap stones or extra opening moves. The result concerns the weak Maker–Breaker game, not the strong game where either player can win by forming the target.

The coordinates label the target cells. The diagram specifies the shape; the recursive certificate below supplies the strategy.

🏷️ Conditional winning statements

A finite conditional statement consists of $(A,T,h)$ with $A\subseteq T$. It asserts that, whenever Maker is to move, owns every cell of $A$, and Breaker owns no cell of $T$, Maker has already won or can win within $h$ further actual claims.

The set $A$ is the required set, $T$ the envelope, and $h$ the height. Additional Maker cells are allowed, as are arbitrary Breaker cells outside $T$. This formulation makes a finite condition useful on an infinite board.

There are six immediate statements: for each $s\in S$, take $A=S\setminus \{s\}$, $T=S$, and $h=1$. If Maker already owns $s$, the target is complete. Otherwise it is free and can be claimed.

Translations and signed coordinate permutations transport any valid statement without changing its height.

🏷️ The combination rule

Suppose $(A_i,T_i,h_i)$ are finitely many valid child statements, and choose a pivot $p$. Define

$$\begin{array}{rl}T& =\{p\}\cup \bigcup _i{T}_i,\\ A& =\left(\bigcup _i{A}_i\cup \bigcap _i{T}_i\right)\setminus \{p\},\\ h& =1+\underset{i}{\max }{h}_i.\end{array}$$

Then $(A,T,h)$ is valid. Here is the full reason. If Maker owns $A$ and Breaker avoids $T$, the pivot is not owned by Breaker. Maker claims it if free. If it is already owned by Maker, Maker makes any fresh replacement claim, counting it as one actual move.

Afterward, Maker owns every child requirement and the entire intersection ${\bigcap }_i{T}_i$. A legal Breaker reply cannot lie in that intersection. Therefore it misses at least one child envelope, whose old Breaker cells were already absent. That child statement applies on the next Maker turn, using at most $h_i$ more claims. Including the pivot or replacement move gives at most $h$.

A reply outside $T$ misses every child envelope. Thus the proof does not impose an artificial finite region on Breaker’s play. If Maker wins during the first claim, the strategy stops immediately.

On the infinite board, a fresh replacement cell exists because a finite history occupies only finitely many cells. For the finite-board conclusion, every descendant envelope and pivot stays inside the final envelope, which the certificate places in a $17\times 17$ board. That board has 289 cells, while the promised win uses at most 41 individual claims. A fresh replacement cell is therefore always available during the relevant play, so the same induction applies.

🏷️ A finite recursive certificate

The paper specifies 728 numbered statements: six immediate bases and 722 further rows using earlier statements and placed copies. Some rows contain nested combinations, giving 1,620 combination nodes in the full reconstruction.

The final statement has

$$\begin{array}{c}A=\varnothing ,|T|=251,\\ h=21.\end{array}$$

It therefore applies from the empty board. Its final pivot is $(8,8)$ and it combines 32 placed children. Their envelopes intersect only in that pivot. This is the finite geometric fact ensuring that one Breaker reply cannot spoil every continuation.

The source turns the recursive proof into a single policy fixed before Breaker plays, by selecting a surviving child according to a fixed rule. A collection of separate favorable responses would not suffice unless these choices were assembled into a legal strategy for every history.

🏷️ Certificate check performed for these notes

The two supplied Python checkers, primary.py and independent.py, were read and run against the pinned 21-move certificate. Both returned PASS. Their reconstructed cards and combination nodes were compared exactly and agreed.

The checks establish the finite reconstruction: 728 cards, 4,089 references, 37,042 reply classes, an empty final required set, a 251-cell final envelope, and height 21. Both check that the final envelope lies in the $17\times 17$ board. The independent implementation also enumerates the eight signed coordinate permutations and checks closure under all 64 compositions.

The certificate’s SHA-256 begins 3fa12d36a6d4dbb1; the complete hash and check summaries are retained in the local audit record. The pinned checker directory contains the two programs and their data.

This is execution of the repository’s supplied finite checkers, together with the combination-rule review above. It is not a Lean build or an independent verification of every theorem and alternative strategy in the manuscript. The older 25- and 35-move routes were not executed here.

🏷️ Key steps and proof outlines

A two-threat example makes the certificate rule concrete

The first nonbase card starts from the five Maker cells

$$A_6=\{(0,y):0\le y\le 4\}$$

and assumes Breaker avoids $T_6=A_6\cup \{(1,3),(1,4),(1,5)\}$. Maker claims the pivot $(1,4)$. The four-cell column at heights zero through three can then be completed by $(1,3)$, while the column at heights one through four can be completed by $(1,5)$, using a reflected target when needed. These are two different cells. Breaker can occupy at most one, so Maker completes a target on the next turn. The card therefore has height two. (OpenAI, 2026)

flowchart TD
    A["Five required cells in a column"] --> P["Maker claims pivot (1,4)"]
    P --> B["Breaker claims (1,3)"]
    P --> C["Breaker claims (1,5)"]
    P --> D["Breaker claims another cell"]
    B --> E["Complete at (1,5)"]
    C --> F["Complete at (1,3)"]
    D --> G["Either completion survives"]

Card seven combines two placed copies of this argument. Their common requirement is the column $\{(0,y):1\le y\le 5\}$, but their additional envelope cells have heights $4,5,6$ and $0,1,2$. Those triples are disjoint. Claiming $(0,5)$ from the four-cell requirement leaves at least one of the two height-two continuations untouched. The new card has height three. The full certificate repeats this elimination of common requirements at much larger scale.

The checker proves set identities, while induction proves their meaning

A card reference consists of an earlier card, one of the eight signed coordinate permutations, and a translation. The transformations are rigid lattice symmetries, so they preserve copies of Snaky. The order of operations matters: the encoding first negates the indicated coordinates, then optionally swaps them, then translates.

Every numbered reference points backward. Parenthesized combinations are evaluated from their innermost expressions outward. Thus the checker maintains an exact invariant: before evaluating row $j$, each stored entry is the requirement set, envelope, and height mathematically defined by its earlier row. A reference transports those finite sets; a combination takes the prescribed unions, intersection, set difference, and maximum. No simulation against a sample of Breaker moves substitutes for this calculation.

Why there are two layers of verification

Exact reconstruction establishes the certificate’s finite set identities. The combination lemma establishes that every such identity implies a valid conditional winning statement. Structural induction connects the two layers, including every inline combination. The final empty requirement then makes the conditional statement applicable to the empty board.

At the final card, all 32 placed child requirements are the pivot $p=(8,8)$. As six groups of children are included, the number of other cells remaining in their common envelope falls through $35,31,21,12,4,0$. Hence both the union of requirements and the intersection of envelopes are exactly $\{p\}$. Removing the pivot leaves the empty requirement. The largest child height is 20, so the final height is 21. This explains which concrete certificate facts are responsible for the opening move and the time bound.

Compile conditional existence into one policy

Fix the printed order of children and an enumeration of the lattice before play. At each active card, claim the placed pivot if free; if Maker already owns it, claim the first free cell instead. The invariant rules out Breaker owning it. After a legal reply, take the first child whose placed envelope avoids that reply. The combination rule guarantees such a child exists, and nesting excludes all earlier Breaker cells as well.

Maintain the placement as an affine map. If the chosen reference uses placement $G$ and the current card uses $F$, the new placement is $F\circ G$. This composition keeps every descendant pivot in the correct coordinate frame. Each nonterminal step uses one actual Maker claim and decreases height, even when the claim is a replacement for an already-owned pivot.

Finally, define the policy on histories inconsistent with its prescribed earlier moves by the same first-free-cell fallback. This makes it a globally defined legal strategy, not a collection of choices depending on future replies. The quantifier order is therefore one fixed strategy against every legal Breaker continuation. The finite-board version uses the nested 251-cell envelope: before Maker’s twenty-first move at most 40 cells are occupied, so replacement moves remain available there. These details are in “The certificate and its final condition” and “One strategy against every continuation.”

See Also

• Cycle–clique Ramsey numbers also separates structural inference rules from a finite certificate, whose computation has a different verification status in these notes.
• Translational tiles uses finite local constraints for an infinite lattice problem, with a different global decoding obligation.

🏷️ Manuscripts and verification scope

• Snaky in 21 Maker moves — pinned manuscript and companion source.

The family scope page describes selected formalization coverage. The main selection is a globally legal 21-move strategy on the infinite board. The other two entries concern the older 35-move certificate and conditional templates. The smaller finite-board conclusion is not part of the selected 21-move statement. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026. Snaky in 21 Maker moves.