we-solve (beta)

Math-2623 · mathematics · Combinatorics

Maker winning strategy for Snaky on the infinite square lattice

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

In the unbiased Maker–Breaker game on the initially empty lattice $\mathbb Z^2$, can Maker force the six-cell Snaky polyomino \[\{(0,0),(1,0),(2,0),(3,0),(3,1),(4,1)\}\] up to translation, rotation or reflection against every legal Breaker strategy?

Short English statement

In the unbiased Maker–Breaker game on the initially empty lattice $\mathbb Z^2$, can Maker force the six-cell Snaky polyomino \[\{(0,0),(1,0),(2,0),(3,0),(3,1),(4,1)\}\] up to translation, rotation or reflection against every legal Breaker strategy?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2623-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2623

The claimed winning policy applies to the exact six-cell target, translation/rotation/reflection conventions and unbiased Maker-first empty infinite-lattice game in the question. Winning within twenty-one Maker claims is stronger than the existence of an unrestricted finite winning strategy.

Maker winning strategy for Snaky on the infinite square lattice

OpenAI's claim

Snaky within 21 Maker claims: The paper claims a Maker strategy for Snaky using at most 21 Maker moves against every legal Breaker response. It can operate on a fixed 251-cell region inside a $17\times17$ square.

Mathematical statement of the claimed result

Mathematical claim 1.
On the initially empty board $\mathbb Z^2$, Maker moves first and each player then claims one unowned cell per turn. For \[S=\{(0,0),(1,0),(2,0),(3,0),(3,1),(4,1)\},\] targets are $t+RS$ with $t\in\mathbb Z^2$ and $R$ a signed permutation matrix, so rotations and reflections but no scaling are allowed. The claim supplies one globally legal Maker policy which, against every legal Breaker continuation, owns an entire target within at most $21$ Maker claims. It therefore asserts a winning strategy for the ordinary unbiased Snaky game.

Outline of the argument

Snaky within 21 Maker claims: Finite winning conditions list required Maker cells, a Breaker-free envelope, and a bound on remaining moves. Backward references combine child conditions after one chosen Maker claim, using envelope intersections to ensure that one Breaker move cannot kill every continuation. A 728-condition certificate closes at the empty initial position; induction extracts a legal policy with the stated move bound.

Formal verification

Family 187 describes Lean coverage for the infinite-board 21-move policy and older conditional certificates; the smaller-board restriction is not selected.

Snaky within 21 Maker claims: The manuscript links SnakyCertificate.lean, SnakyConditional.lean, SnakyTwentyOne.lean.

The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

Go to contribution →