# Snaky in 21 Maker moves

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

- [Snaky in 21 Maker moves](../../preprints/Snaky-in-21-Maker-moves-September-25-2026/article.pdf)

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

| Result | Comparator statement |
| --- | --- |
| Reconstruction of the 35-move Snaky certificate | [SnakyCertificate.lean](../ComparatorChallenges/SnakyCertificate.lean) |
| Conditional winning templates from finite partial positions | [SnakyConditional.lean](../ComparatorChallenges/SnakyConditional.lean) |
| Legal Snaky winning strategy within 21 Maker moves | [SnakyTwentyOne.lean](../ComparatorChallenges/SnakyTwentyOne.lean) |