Pre-release GPT-6 Astra disproves Erdős’s ‘first serious problem’ (1931, $500) and proves the rational-exponents conjecture, all Lean-verified, in Epoch’s FrontierMath Erdős runs
Result confirmed
Importance: historic (5 of 5)The takeaway
In Epoch AI’s FrontierMath Erdős runs (announced 3 Sep 2026), a pre-release GPT-6 Astra autonomously resolved five of 68 hand-picked open Erdős problems with Lean-checked proofs.
Status
- Claim
Result confirmed
- Our reporting
- High confidence
- Verification
- Lean-verified
- Importance
- Historic (5 of 5)
- Last verified
- 16 October 2026
Your AI and this story
- GPT-6 Astra126 days after its cutoff
- Claude Opus 5.565 days after its cutoff
- Gemini 4 Hydrogen156 days after its cutoff
- Grok 4.795 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 65 days before it.
Key facts
- Benchmark: 68 open Erdős problems chosen by Thomas Bloom from 652 open problems on erdosproblems.com; a resolution counts only if it is proved in Lean; default budget $300 and 72 hours per problem
- Official score (one attempt each): pre-release GPT-6 Astra 3% (#74 disproved for $218 in 15 h; #126 proved for $247 in 16 h); GPT-5.6 Sol, GPT-5.5, Claude Fable 5.1 and Claude Fable 5 all 0%
- Extra, non-benchmark attempts with larger budgets resolved 5 problems in total (#1, #74, #126, #548, #571), using over $220,000 of compute versus about $20,000 for the benchmark run
- #1 (Erdős, dated 1931, $500 prize): if A ⊆ {1..N} has n elements with all subset sums distinct, must N ≫ 2^n? Astra showed that for every ε > 0 there are arbitrarily large n with N ≤ ε·2^n, so the conjecture is false. The previous best construction was N ≤ 0.22002·2^n (Bohman). The proof is ineffective (no explicit n for a given ε). Found in 2 of 4 attempts ($405 / 27 h and $1,384 / 84 h)
- #571 (Erdős–Simonovits): for every rational α in [1,2) there is a bipartite graph G with ex(n; G) ≍ n^α. Bloom calls it ‘the most difficult of the five solutions’. Found in 1 of 3 attempts ($617, 41 h)
- #74 (Erdős–Hajnal–Szemerédi): disproved in the unexpected direction. If every n-vertex subgraph can be made bipartite by deleting at most f(n) edges with f growing slowly enough, the graph has chromatic number ≤ 3
- #126 (Erdős–Turán): |S(A)| ≫ n^(1/2) primes divide the pairwise sums of an n-element set, improving the classical log n bound; Astra gave three distinct proofs (exponents 1/8, 1/3 and 1/2)
- erdosproblems.com now marks #1 as ‘DISPROVED (LEAN)’
Show 2 more
- The Lean repositories (tadamcz/erdos1, erdos74, erdos126, erdos571), created 3 Sep 2026, say the proofs were found autonomously in the benchmark harness; the report calls the informal write-ups ‘placeholders’ until human experts prepare proper papers
- Also published (repo tadamcz/erdos1207, created 7 Sept 2026): Erdős problem #1207 (isosceles-free subsets, attributed to Riddell) proved: there is c > 0 with P_2(n) < n^(1−c), i.e. for large n some n-point planar sets have no isosceles-free subset larger than n^(1−c) (a power saving that Erdős asked for); ‘found autonomously by a pre-release version of GPT-6 Astra … running in the harness of the FrontierMath Erdős benchmark’; Lean 4 proof with an audit script; repository ‘machine-written by AI assistants at the direction of Tom Adamczewski’; not counted in the five problems above and not independently reviewed
What happened
Epoch AI and Thomas Bloom (erdosproblems.com) built FrontierMath Erdős, a benchmark of 68 open Erdős problems formalised in Lean, and ran five frontier models on it. Under the fixed $300 budget only the pre-release GPT-6 Astra solved anything (2 of 68). In further runs with larger budgets, which the authors report separately and do not count as benchmark results, Astra also disproved problem #1, proved the Erdős–Sós conjecture (#548) and proved the rational-exponents conjecture (#571). Every resolution comes with a Lean proof checked against a small challenge statement.
Why it matters
Problem #1 is probably the longest-standing open Erdős problem. The #571 result settles a central question on Turán numbers of bipartite graphs. The paper also gives a denominator that most AI-math announcements lack. The fixed-budget run solved only 2 of 68 problems. Of the 63 unsolved problems, 56 were retried two to five times each (172 attempts) with no success, and the five resolutions took over $220,000 of compute. That makes it a sober counterweight to OpenAI’s later claim of “100+ open problems”.
Follow-up: expert write-up of #571 (13 Oct)
On 13 Oct 2026 eight extremal combinatorialists (Conlon, Janzer, Jiang, Kim, Lee, Liu, Longbrake, Yepremyan) posted arXiv 2610.187135, which explains and situates the #571 proof “claimed by Epoch AI, obtained during benchmarking for the recently released model GPT-6 Astra”. It replaces the placeholder write-up with a human paper; see its own entry.
Sources
10 sources from 5 sites. Numbers match the chips in the text.
10 sources: 7 primary, 1 press, 2 reactions
Primary
- GitHub: tadamcz/erdos1207 (Lean proof of Erdős #1207 by GPT-6 Astra)github.com, code
- arXiv 2609.25050: FrontierMath Erdős (Adamczewski, Bloom)arxiv.org, paper
- GitHub: tadamcz/erdos1 (Lean disproof)github.com, code
- GitHub: tadamcz/erdos571 (rational exponents, Lean proof)github.com, code
- arXiv 2610.18713: A proof of the rational exponents conjecture (Conlon, Janzer et al., expert write-up of #571)arxiv.org, paper
- GitHub: tadamcz/erdos74github.com, code
- GitHub: tadamcz/erdos126github.com, code
Press
- Quanta: Why Erdős Problems Are Falling to AI (3 Aug 2026)quantamagazine.org, press
Reactions
- erdosproblems.com #1 (status: disproved, Lean)erdosproblems.com, discussion
- Thomas Bloom on X: A big day for AI and mathematics (3 Sep 2026)x.com, discussion
Changes
- Added Erdős #1207 (repo tadamcz/erdos1207), found while checking the Oct 16 lead on Epoch’s LeanOpenProblems runs
- Added the expert write-up of the #571 proof (arXiv 2610.18713) as a follow-up
- Science block: short label (normalised Erdős problem labels)
- Filed