Harary's Snaky problem: is the Snaky hexomino a winner in the planar Maker-Breaker achievement game?
In Harary's polyomino achievement games two players alternately claim cells of the infinite square grid; Maker wins on owning a translated, rotated or reflected copy of a fixed polyomino. The target is the hexomino Snaky, . Known: no pairing defense for Breaker, a win in 41 and in three dimensions, a loss on the board, and a planar win with handicap one (Halupczok-Schlage-Puchta, Ito-Miyagawa, Sieben). Can Maker, moving first on the empty infinite plane with no handicap, force a copy of Snaky?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Combinatorial games; polyomino achievement games
- Posed by
- Frank Harary (polyomino achievement games, as attributed by Sieben 2004); the ordinary planar case recorded as undecided by Nandor Sieben (Integers 8, 2008)
- Year posed
- —
- Years open
- —
- Solved
- 2026-09-25
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 20 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1: one globally legal Maker policy completes Snaky within 21 Maker claims (by the 41st turn) against every legal Breaker play on the empty infinite board, so Snaky is a winner in the planar weak game. It works on a board, using a fixed 251-cell region; 25- and 35-move constructions are also given. Not shown: optimal move count or board size, or the strong game in which both players seek a copy.
What the AI did
Produced by an unreleased internal OpenAI model as part of OpenAI's openai/math release. The release README says the results used one fixed procedure averaging about three hours of ChatGPT Pro thinking compute per result; this family is not among the README's stated exceptions (the Hodge conjecture for CM abelian varieties and the Re(s) > 11/12 zero-free region). The manuscripts are authored as OpenAI with no human author named.
Verification
No independent mathematician has checked this yet. Checked here: abstract, introduction and Theorem 1, read against the planar Snaky question as cited; the 728-condition certificate was not rechecked. Lean-checked on the release's Comparator challenge SnakyTwentyOne with solution module OAI.GameTheory.SnakyTwentyOne.Main, both fetched at the pinned commit; the challenge is not listed in lean/formalization.yaml. Statement read here, not rebuilt: it defines Snaky, its eight orientations and translates, and asserts a Maker policy that always picks free cells and, against every Breaker sequence legal for the first 20 replies, owns a copy of Snaky after 21 claims with disjointness and move counts tracked. That is the headline. Two further challenges formalize the 35-move certificate and conditional templates.