The γ–θ conjecture in eternal domination
The – conjecture asserts that for every finite graph ,where is the domination number, is the eternal domination number in the one-guard-moves model, and is the vertex clique-cover number.
The conjecture is false. The complement of the 243-vertex ternary Golay graph satisfies
- Result
- Disproved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Graph theory
- Posed by
- William F. Klostermeyer and C. M. Mynhardt
- Year posed
- 2014
- Years open
- 12y
- Solved
- 2026-09-05
- Model
- GPT-6 Astra (pre-release)
- Vendor
- OpenAI
- Collaborators
- Tom Adamczewski
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 12 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Let be the Berlekamp–van Lint–Seidel graph on vertices, the Cayley graph of with strongly regular parametersand let .
The proof establishesbecause every pair has a common neighbor in , while an -triangle gives a dominating triple in .
It then provesby showing that the family of all dominating triples is closed under a legal response to every attack: after moving one guard to the attacked vertex, another dominating triple can always be obtained.
Finally, a double-counting argument shows that is not 3-colorable, henceTherefore
What the AI did
GPT-6 Astra found the counterexample and wrote the Lean proof. It recognized that the complement of the classical 243-vertex Berlekamp–van Lint–Seidel ternary Golay graph provides the needed structure, proved , constructed an indefinitely repeatable three-guard defense proving , and proved by a coloring/double-counting argument. The underlying Golay graph was known since 1973; the new contribution is identifying its complement as a counterexample and proving the eternal domination strategy.
Verification
Lean-checked, statement unaudited. Checked here on 6 September 2026 from a clone of tadamcz/gamma-theta at d64cce5: 1,987 lines; the only sorry outside Challenge.lean is the unused '.disproof' stub in submission/Spec.lean, which the README explains (the compared theorem asserts the existence of the counterexample); zero axiom declarations, no native_decide; the audit folder's docker logs print the theorem's axioms as the standard three. The statement was AI-autoformalized in Epoch's wikipedia run; the definitions of the eternal dominating family (one-guard model), domination number and clique cover number were read here and look right, but that is one reading, not an audit. The repository's Python check of 5,889,840 attacks was not replayed here.
Sources
- Lean proofThe Lean development
- Lean statementChallenge.lean: the compared statement and definitions
- CodeGithub
Submitted by VibeGene on