GPT-6 Astra's Epoch AI run adds more Lean-checked results: Dittert conjecture proved, Ibragimov–Iosifescu and eternal-domination conjectures disproved

2026-09-10★★★after cutoffscienceOpenAIEpoch AIconfidence: medium

After the Köthe disproof, the same September 2026 Epoch AI run of pre-release GPT-6 Astra over the Formal Conjectures collection produced more machine-written Lean results, published by Tom Adamczewski: a proof of the full Dittert permanent conjecture, a counterexample to the Ibragimov–Iosifescu φ-mixing CLT conjecture, a disproof of the strong n-conjecture for n=4, and a 243-vertex graph refuting the Gamma–Theta eternal-domination conjecture (arXiv 2609.11500, with William Klostermeyer). Most results have not had independent expert review.

Key facts

Setting: Epoch AI's LeanOpenProblems harness; pre-release GPT-6 Astra tried each research-open Formal Conjectures statement once, autonomously (see the Köthe entry)
Dittert conjecture: φ(A) ≤ 2 − n!/n^n for nonnegative n×n matrices with entries summing to n, with equality only for the all-1/n matrix. Lean proof passed the Comparator check (repo tadamcz/dittert); the exposition is not independently reviewed. Humans had earlier proved n ≥ 17 (arXiv 2606.01531) and n = 16 (arXiv 2607.19439, GPT-5.6 Sol-assisted)
Ibragimov–Iosifescu conjecture (Ibragimov, 1971): disproved with a strictly stationary φ-mixing counterexample; a 13,047-line Lean proof, 'Lean-checked, statement unaudited', announced 5 Sep 2026 (repo tadamcz/phi-mixing-clt)
Strong n-conjecture, n = 4: disproved in Lean with extra SymPy arithmetic checks (repo tadamcz/n-conjecture-strong)
Eternal domination: 243-vertex graph with γ(G) = γ∞(G) < θ(G), refuting the Gamma–Theta conjecture. Tom Adamczewski & William F. Klostermeyer, arXiv 2609.11500, 10 Sep 2026
The repositories say they were 'machine-written by AI assistants at the direction of Tom Adamczewski'

Science result

Field: mathematics / combinatorics / matrix theory / probability / number theory
Problem: Dittert conjecture; Ibragimov–Iosifescu φ-mixing CLT conjecture; strong n-conjecture (n=4); Gamma–Theta eternal domination conjecture
Result: One proof (Dittert, all n) and three disproofs, each with a Lean formalization or an explicit checkable counterexample.
AI system: GPT-6 Astra (pre-release)
Human role: Autonomous proof search in Epoch AI's harness; Tom Adamczewski directed packaging; Klostermeyer co-wrote the domination paper
Verification: Formal proofs in Lean (mechanically checked). Statements and write-ups mostly not independently audited
Status: pending

What happened

Epoch AI ran pre-release GPT-6 Astra once on each research-open statement in the Formal Conjectures collection. Besides Köthe, several more outputs were packaged as Lean repositories by Tom Adamczewski in the first half of September 2026. For the graph-theory counterexample, domination expert William Klostermeyer co-wrote an arXiv paper.

Why it matters

Autonomous formal proof search now turns out a steady stream of mid-level resolved conjectures, not one-off headlines. The bottleneck is shifting to human auditing of whether the formal statements are the intended ones.

Changelog

2026-09-29: created (grouped several September 2026 Astra/Epoch results)

Related events

2026-09-07Pre-release GPT-6 Astra disproves the Köthe conjecture (1930) with a Lean-verified counterexample ★★★★
2026-09-03OpenAI releases GPT-6 Astra, its first GPT-6 model ★★★★★
2026-08-30GPT-6 Astra lowers the bounded prime gaps record from 246 to 186 ★★★★
2026-09-21OpenAI says an internal model resolved 100+ long-standing open problems in 24 days of training; no list released ★★★
2026-08-26GPT-5.6 improves the Erdős–Rankin / Ford–Green–Konyagin–Maynard–Tao bound for large prime gaps ★★★★

Sources (6)

id: 2026-09-10-astra-leanopenproblems-september-results · updated 2026-09-29 · open in the interactive timeline