VibeMathedMath problems solved with AI

The γ–θ conjecture in eternal domination

The γ\gammaθ\theta conjecture asserts that for every finite graph GG,γ(G)=γ(G)γ(G)=θ(G), \gamma(G)=\gamma^\infty(G) \quad\Longrightarrow\quad \gamma(G)=\theta(G), where γ\gamma is the domination number, γ\gamma^\infty is the eternal domination number in the one-guard-moves model, and θ\theta is the vertex clique-cover number.

The conjecture is false. The complement GG of the 243-vertex ternary Golay graph satisfiesγ(G)=γ(G)=3<θ(G). \gamma(G)=\gamma^\infty(G)=3<\theta(G).

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 HH be the Berlekamp–van Lint–Seidel graph on 243243 vertices, the Cayley graph of Z35\mathbb Z_3^5 with strongly regular parameters(243,22,1,2), (243,22,1,2), and let G=HG=\overline H.

The proof establishesγ(G)=3 \gamma(G)=3 because every pair has a common neighbor in HH, while an HH-triangle gives a dominating triple in GG.

It then provesγ(G)=3 \gamma^\infty(G)=3 by 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 HH is not 3-colorable, henceθ(G)=χ(H)>3. \theta(G)=\chi(H)>3. Thereforeγ(G)=γ(G)=3<θ(G). \gamma(G)=\gamma^\infty(G)=3<\theta(G).

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 γ=3\gamma=3, constructed an indefinitely repeatable three-guard defense proving γ=3\gamma^\infty=3, and proved θ>3\theta>3 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

Submitted by VibeGene on

Changelog2 changes

Discussion