--- id: "2026-09-10-astra-leanopenproblems-september-results" url: "https://postcutoff.com/e/2026-09-10-astra-leanopenproblems-september-results/" as_of: "2026-11-13T13:49:00+01:00" date: "2026-09-10" date_precision: day category: science importance: 3 confidence: medium status: [Awaiting review] verification: "Lean proof, not yet reviewed" sources: 6 editor: human editor human_review: null version: "2026-10-19" --- As of: 2026-11-13 13:49 CET. Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/ Canonical page: https://postcutoff.com/e/2026-09-10-astra-leanopenproblems-september-results/ # GPT-6 Astra's Epoch AI run adds more Lean-checked results Full title: GPT-6 Astra's Epoch AI run adds more Lean-checked results: Dittert conjecture proved, Ibragimov–Iosifescu and eternal-domination conjectures disproved 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' - Same run, Wikipedia collection ('wikipedia-vega-1000usd', all 222 research-open statements, $1,000 and 96 h each): disproof of Smale's mean value conjecture for K = 1 (repo tadamcz/mean-value-problem; own entry [2026-09-03-smale-mean-value-conjecture-disproved-gpt-6-astra](https://postcutoff.com/e/2026-09-03-smale-mean-value-conjecture-disproved-gpt-6-astra/index.md)). Epoch's LeanOpenProblems README publishes no overall solved count (checked 16 Oct) ## 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. ## What is disputed or not yet verified - Verification: Formal proofs in Lean (mechanically checked). Statements and write-ups mostly not independently audited ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 133 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 72 days after its cutoff - Gemini 4 Hydrogen (training cutoff March 2026): 163 days after its cutoff - Grok 4.7 (training cutoff May 2026): 102 days after its cutoff ## Sources 1. [arXiv 2609.11500: A Counterexample to an Eternal Domination Conjecture](https://arxiv.org/abs/2609.11500) (arxiv.org, paper) 2. [GitHub: tadamcz/dittert](https://github.com/tadamcz/dittert) (github.com, code) 3. [GitHub: tadamcz/phi-mixing-clt (Ibragimov–Iosifescu)](https://github.com/tadamcz/phi-mixing-clt) (github.com, code) 4. [GitHub: tadamcz/n-conjecture-strong](https://github.com/tadamcz/n-conjecture-strong) (github.com, code) 5. [VibeMathed: Ibragimov–Iosifescu conjecture status](https://vibemathed.com/problem/ibragimov-iosifescu-varphi-mixing-clt-conjecture) (vibemathed.com, discussion) 6. [Wikipedia: List of mathematical discoveries by artificial intelligence](https://en.wikipedia.org/wiki/List_of_mathematical_discoveries_by_artificial_intelligence) (en.wikipedia.org, discussion) ## Changes - 2026-10-19: Related: back-links to the Smale mean value and Köthe entries - 2026-10-16: Linked the Smale mean-value disproof from the same run; noted that Epoch publishes no overall results count - 2026-09-29 (filed): Created (grouped several September 2026 Astra/Epoch results) ## Related - 2026-09-21: [OpenAI says an internal model resolved 100+ long-standing open problems in 24 days of training (list released 6 Oct: 722 manuscripts)](https://postcutoff.com/e/2026-09-21-openai-100-open-problems-claim/index.md) - 2026-09-07: [Pre-release GPT-6 Astra disproves the Köthe conjecture with a Lean-verified counterexample](https://postcutoff.com/e/2026-09-07-koethe-conjecture-disproved/index.md) - 2026-09-03: [OpenAI releases GPT-6 Astra, its first GPT-6 model](https://postcutoff.com/e/2026-09-03-gpt-6-astra/index.md) - 2026-09-03: [GPT-6 Astra autonomously disproves Smale's mean value conjecture in Lean](https://postcutoff.com/e/2026-09-03-smale-mean-value-conjecture-disproved-gpt-6-astra/index.md) - 2026-08-30: [GPT-6 Astra lowers the bounded prime gaps record from 246 to 186](https://postcutoff.com/e/2026-08-30-bounded-prime-gaps-186/index.md)