Tracker · updated 2026-10-08

AI results on open problems: a tracker

Results on genuinely open mathematics problems where an AI system produced the key argument or object, with how each was checked. Compiled from public sources; every row links to them. Successes get announced and failures usually do not, so read this as a list of claims and verifications, not a success rate.

Checked by

Who drove it

14 of 14 results

2026-10-06

Batch release of new results from an internal OpenAI model

claimed onlyAI-ledbatch

System: Internal OpenAI frontier model · Who: OpenAI · Various

Published in a GitHub repository: 722 manuscripts in 372 result families, from about 4,000 problems posed to the model. Many, but not all, manuscripts come with Lean formalizations; the release also includes ten reasoning summaries and compute estimates. OpenAI says the average result used compute equal to about three hours of ChatGPT Pro thinking, and that it consulted the IAS Advisory Group on Mathematics and AI on release practices.

Status: Released; community review just starting

Caveat: OpenAI says some of the unformalized results could have issues, so the release as a whole is a claim; formalized results are checked individually. Quanta reported the day before that OpenAI was holding back more than 100 results; the release covers more (372 families).

OpenAI: Sharing AI progress in mathematics (Oct 6, 2026)Quanta: Is AI the End of Math As We Know It? (Oct 5, 2026)GitHub: openai/math (the release)

2026-09

Erdős #1 (distinct subset sums) disproved

Lean / Isabelleautonomousdisproofopen since 1931

System: GPT-6 Astra (pre-release) · Who: OpenAI model; Epoch AI evaluation · Additive combinatorics

Erdős called it “perhaps my first serious problem”. The model built dissociated sets in {1,…,N} with N ≤ ε·2ⁿ for any ε > 0, refuting the conjectured N ≫ 2ⁿ. Bloom reinterpreted the proof in terms of lattices.

Status: Lean-verified; human write-up pending

Caveat: Resolved in 2 of 4 attempts ($405, 27 h; $1,384, 84 h). The $405 disproof came in the benchmark run but is unscored: at Astra’s actual prices it exceeded the $300 cap. The proof is currently ineffective in n.

Adamczewski & Bloom, FrontierMath Erdős (Epoch AI)

2026-09

Erdős–Sós conjecture (#548) proved

Lean / Isabelleautonomousproofopen since 1962

System: GPT-6 Astra (pre-release) · Who: OpenAI model; Epoch AI evaluation · Extremal graph theory

Every graph on n vertices with more than (k−2)n/2 edges contains every tree on k vertices. Bloom describes the proof as surprisingly short: a double count of (vertex ordering, label) pairs.

Status: Lean-verified; human expositions published

Caveat: Resolved in 1 of 3 attempts ($363, 20 hours), outside the scored benchmark run. Relation to the large prior literature still being assessed.

Adamczewski & Bloom, FrontierMath Erdős (Epoch AI)Riordan & Scott: A short proof of the Erdős–Sós conjecture (arXiv:2609.15893)

2026-09

FrontierMath Erdős: #74 disproved, #126 and #571 proved

Lean / Isabelleautonomousmixed

System: GPT-6 Astra (pre-release); also tested GPT-5.6 Sol, GPT-5.5, Claude Fable 5 and 5.1 · Who: Epoch AI with Thomas Bloom · Graph theory, number theory

68 hand-picked open Erdős problems, each stated in Lean; one attempt per problem, $300 and 72 hours. Astra resolved 2 of 68 (3%), every other model 0. #126 now has a lower bound ≫ √n, far beyond the asked-for growth faster than log n. #571 (Erdős–Simonovits rational exponents) was proved only in an extra attempt (1 of 3, $617) and is, in Bloom’s view, the hardest of the five.

Status: Lean-verified (Comparator)

Caveat: All five resolutions together took over $220,000 of compute across attempts. Formal proofs are certain but not yet digested by humans.

Adamczewski & Bloom, FrontierMath Erdős (Epoch AI)Benchmark repo: epoch-research/LeanOpenProblems

2026-09-08

Navier–Stokes finite-time blowup (claimed)

claimed onlyAI-leddisproof (of global smoothness)open since 2000 (Clay Millennium Problem)

System: Internal OpenAI model described as significantly more capable than GPT-6 Astra; the winning group ran about 10,000 concurrent agents, with the result about 88 hours after the first launch · Who: OpenAI · PDE

A 166-page paper (an earlier private description put the proof at about 100 pages) arguing that an initially smooth fluid driven by a smooth force can develop a singularity in finite time. OpenAI says the agents were seeded with its own unforced-Euler blowup result and used Codex to merge insights across groups.

Status: Claimed with a Lean formalization; not independently verified; Clay has not verified or recognized it; disputed

Caveat: Many mathematicians question whether a forced result answers the Clay problem as they understand it. OpenAI recognizes Alpöge and Buckmaster’s priority on forced Euler blowup; Buckmaster says OpenAI followed the route they were pursuing, and OpenAI denies seeing their work before its release.

OpenAI: On the Navier–Stokes Millennium Prize Problem Implicator: forcing and credit questions The Print: Buckmaster’s account

2026-08-15

Euler equations blowup (forced)

Lean / Isabellehuman–AIconstruction

System: AI-assisted; reports name both Anthropic models and OpenAI tools · Who: Tristan Buckmaster (NYU) and Levent Alpöge (Anthropic employee), as personal research · PDE

Finite-time singularity for the Euler equations (no viscosity), a step toward Navier–Stokes. Terence Tao called it a remarkable achievement and saw no fundamental obstacle to extending the methods.

Status: Results obtained Aug 15 and Lean-checked Aug 22 by the authors’ account; papers posted publicly Sept 7

Caveat: Accounts of which AI tools did what differ between sources. Buckmaster has said the AI-produced write-up was hard to read and had to be reworked by hand. OpenAI separately claims an unforced Euler blowup (early September) and recognizes this pair’s priority on forced Euler.

AI Weekly summary of Scientific American reporting Lilting: timeline of the dispute Terence Tao on the Euler blowup (Mathstodon)

2026-08-01

Ten advances in mathematics and theoretical computer science

Lean / IsabelleAI-ledbatch

System: Internal version of Astra (OpenAI’s next major model) · Who: OpenAI · Geometry, coding theory, group theory, operator algebras, complexity, cryptography, combinatorics

Includes new sphere-packing upper bounds, exponentially better binary-code bounds, existence of non-sofic groups, a disproof of Connes’s rigidity conjecture, an n⁴/log n formula lower bound for the permanent, exponential quantum parallel repetition, polynomial-factor hardness for the closest vector problem, Ehrhart’s volume conjecture, and Erdős #183, #146 and #180. Finding all ten took tokens worth about $2,000 in total at Sol API rates.

Status: Lean certificates published; manuscripts prepared by people with the model

Caveat: The problems were selected by OpenAI and the number of unsuccessful attempts was not reported.

OpenAI: Ten advances in mathematics Lean certificates: github.com/openai/ten-proofs

2026-07-20

Jacobian conjecture false for n ≥ 3

Lean / Isabellehuman–AIdisproofopen since 1939

System: Claude Fable 5 · Who: Levent Alpöge (Anthropic); his announcement credits Akhil Mathew with prompting the question · Algebraic geometry

An explicit degree-7 polynomial map of ℂ³ with Jacobian determinant −2 everywhere that sends three points to (−1/4, 0, 0). Padding with identity gives counterexamples in every dimension ≥ 3.

Status: Accepted; formalized in the Isabelle Archive of Formal Proofs; n = 2 still open

Caveat: No prompt transcript or search log has been published, so the human and AI contributions are not documented.

Isabelle AFP: Jacobian_Counterexample John D. Cook: Locally everywhere does not imply everywhere

Interactive walkthrough

2026-05

Sum–product conjecture false over the reals

expert reviewhuman, AI-inspireddisproof

System: GPT-5.5 Pro as a sounding board (it suggested one lemma); the argument is human, inspired by the unit-distance disproof · Who: Bloom, Sawin, Schildkraut, Zhelezov · Additive combinatorics

A set of real numbers whose sumset and product set both grow more slowly than the conjecture predicted, found within a week of the unit-distance result using related ideas.

Status: Preprint; the integer version remains open

Caveat: Listed as a follow-on: the argument is human-written.

arXiv:2605.28781

2026-05

Formal proof search on 353 formalized Erdős statements

Lean / Isabelleautonomousmixed

System: AlphaProof Nexus agent (Gemini 3.1 Pro + AlphaProof) · Who: Google DeepMind (Tsoukalas et al.) · Number theory, combinatorics

The agent resolved 9 of 353 formalized statements at a few hundred dollars each. Four problems were settled outright (#152, #846, #125, #26); others were variants or single readings of ambiguous statements.

Status: Lean-verified

Caveat: The attempted set was whatever the community had formalized, not chosen for interest; several resolved statements are partial versions. “A few hundred dollars” is per solved problem and excludes the search over all 353.

arXiv:2605.22763 Epoch AI, FrontierMath Erdős §2 (context)

2026-05-20

Erdős unit distance conjecture (#90) disproved

Lean / IsabelleAI-leddisproofopen since 1946

System: Internal OpenAI general-purpose reasoning model · Who: OpenAI · Discrete geometry

Point sets with n^{1+δ} unit distances for a fixed δ > 0, using CM number fields of growing degree from class field towers. The original proof gave no explicit δ; the companion paper’s digest gets 1 + 6.24×10⁻³⁸. Gowers: had a human submitted it to the Annals, he would have recommended acceptance.

Status: Accepted; human-digested version by nine mathematicians; Sawin improved it to n^1.014 the same day

Caveat: The first Lean formalization (Logical Intelligence’s Aleph Prover, about 33,000 lines) is conditional on two textbook class-field-tower theorems not yet in Mathlib; unconditional versions were reported later on erdosproblems.com. The model’s write-up did not cite closely related literature (Wood).

OpenAI: model disproves discrete geometry conjecture Alon et al., Remarks on the disproof (arXiv:2605.20695)Quanta: Why the Legendary Erdős Problems Are Falling to AI Sawin: improvement to n^1.014 (arXiv:2605.20579)Logical Intelligence: Aleph Prover formalizes the unit-distance disproof in Lean 4

Interactive walkthrough

2026-04

Erdős #1196 (primitive sets) resolved

expert reviewAI-ledproof

System: GPT-5.4 Pro · Who: Liam Price (prompt); paper with Tao, Lichtman, Barreto and others · Number theory

From a single prompt, the model found a route unlike Erdős’s probabilistic framing that leads to a proof in under a page. Tao suggested earlier attempts may have hit a mental block.

Status: Paper with human co-authors

Caveat: The raw model output needed expert interpretation before it was usable.

arXiv:2605.00301 Physics World: AI-led solutions of Erdős problems Scientific American: An amateur just solved a 60-year-old math problem by asking AI

2026-01

Aletheia sweep of 700 open Erdős problems

expert reviewAI-ledmixed

System: Aletheia (agent on Gemini Deep Think) · Who: Google DeepMind · Number theory, combinatorics

4 novel solutions, including fully autonomous ones for #652 and #1051, and 9 problems found already solved in old literature. The #1051 solution led to a generalization paper.

Status: Published; prompts and raw responses released for the highlighted problems

Caveat: Counts from the paper body (its abstract gives slightly different numbers). Of 212 responses flagged as possibly correct (200 definitively graded), 63 were technically correct but only 13 meaningfully addressed the intended problem. The authors attribute many successes to obscurity rather than difficulty.

Feng et al., Semi-Autonomous Mathematics Discovery with Gemini (arXiv:2601.22401)Towards Autonomous Mathematics Research (arXiv:2602.10177)

2026-01

Erdős #728 (factorial divisibility) resolved

Lean / IsabelleAI-ledproof

System: GPT-5.2 Pro; proof formalized in Lean with Harmonic’s Aristotle · Who: Kevin Barreto and Liam Price (prompting and formalization); write-up by Nat Sothanaphan · Number theory

One of the first cases where no prior solution turned up after an AI resolution. Tao described it as solved almost autonomously.

Status: Accepted on erdosproblems.com

Caveat: About ten days earlier, Barreto’s claimed first win (#333) turned out to be already implied by a 1977 Erdős–Newman paper: a reminder to search the literature first.

Sothanaphan, write-up of Aristotle’s Lean proof (arXiv:2601.07421)Tao’s wiki: AI contributions to Erdős problems Terence Tao on #728 (Mathstodon)

Benchmarks at a glance

Benchmark	What it measures	Best reported	As of
FrontierMath Tier 4 (v2, 43 problems)	Research-level problems with known answers	GPT-6 Astra 97.6%; Claude Fable 5 ≈ 88–90% (trackers differ); GPT-5.6 Sol 83% Saturated in Epoch’s sense: across all models’ attempts, every problem has now been solved at least once; no single model has a perfect score.	Sep 2026
FrontierMath: Open Problems (49)	Unsolved problems with computer-checkable answers	5 solved by AI alone and 5 by human + AI; 39 unsolved Epoch estimates 10–40% may have no solution of the required form.	Oct 2026
FrontierMath Erdős (68)	Open Erdős problems; must prove or disprove in Lean	GPT-6 Astra (pre-release) 3%; four other models 0% $300 and 72 hours per problem, one attempt each.	Sep 2026
First Proof, round 2 (10)	Unpublished research problems, refereed double-blind	7 of 10 problems got at least one passing grade across four AI systems Graded by about 30 expert referees.	Jun 2026

How to read a claim

Search the literature first: several early “AI solutions” were rediscoveries of old papers.
Prefer results with a checkable object or a formal proof; expert review is slower and scarcer.
Ask for the denominator: how many problems were tried, at what cost, with how much human steering.
A formal proof shows the theorem is true; humans still have to work out why, and how it connects to what was known.

Labels

Checked by

Lean / Isabelle: Machine-checked (Lean or Isabelle)
checkable object: Explicit object anyone can check
expert review: Checked by named experts
claimed only: Claimed; not yet independently verified

Who drove it

autonomous: Autonomous: fixed harness, no human guidance
AI-led: AI-led: people chose or prompted the problem; AI produced the argument
human–AI: Human–AI collaboration; division of labor not fully documented
human, AI-inspired: Human result built on AI-found techniques

Compiled from public sources linked on each row. The data is also available as tracker.json. Corrections welcome.

AI results on open problems: a tracker

Checked by

Who drove it

14 of 14 results

2026-10-06

Batch release of new results from an internal OpenAI model

claimed onlyAI-ledbatch

System: Internal OpenAI frontier model · Who: OpenAI · Various

Status: Released; community review just starting

OpenAI: Sharing AI progress in mathematics (Oct 6, 2026)Quanta: Is AI the End of Math As We Know It? (Oct 5, 2026)GitHub: openai/math (the release)

2026-09

Erdős #1 (distinct subset sums) disproved

Lean / Isabelleautonomousdisproofopen since 1931

System: GPT-6 Astra (pre-release) · Who: OpenAI model; Epoch AI evaluation · Additive combinatorics

Status: Lean-verified; human write-up pending

Adamczewski & Bloom, FrontierMath Erdős (Epoch AI)

2026-09

Erdős–Sós conjecture (#548) proved

Lean / Isabelleautonomousproofopen since 1962

System: GPT-6 Astra (pre-release) · Who: OpenAI model; Epoch AI evaluation · Extremal graph theory

Every graph on n vertices with more than (k−2)n/2 edges contains every tree on k vertices. Bloom describes the proof as surprisingly short: a double count of (vertex ordering, label) pairs.

Status: Lean-verified; human expositions published

Caveat: Resolved in 1 of 3 attempts ($363, 20 hours), outside the scored benchmark run. Relation to the large prior literature still being assessed.

Adamczewski & Bloom, FrontierMath Erdős (Epoch AI)Riordan & Scott: A short proof of the Erdős–Sós conjecture (arXiv:2609.15893)

2026-09

FrontierMath Erdős: #74 disproved, #126 and #571 proved

Lean / Isabelleautonomousmixed

System: GPT-6 Astra (pre-release); also tested GPT-5.6 Sol, GPT-5.5, Claude Fable 5 and 5.1 · Who: Epoch AI with Thomas Bloom · Graph theory, number theory

Status: Lean-verified (Comparator)

Caveat: All five resolutions together took over $220,000 of compute across attempts. Formal proofs are certain but not yet digested by humans.

Adamczewski & Bloom, FrontierMath Erdős (Epoch AI)Benchmark repo: epoch-research/LeanOpenProblems

2026-09-08

Navier–Stokes finite-time blowup (claimed)

claimed onlyAI-leddisproof (of global smoothness)open since 2000 (Clay Millennium Problem)

Status: Claimed with a Lean formalization; not independently verified; Clay has not verified or recognized it; disputed

OpenAI: On the Navier–Stokes Millennium Prize Problem Implicator: forcing and credit questions The Print: Buckmaster’s account

2026-08-15

Euler equations blowup (forced)

Lean / Isabellehuman–AIconstruction

System: AI-assisted; reports name both Anthropic models and OpenAI tools · Who: Tristan Buckmaster (NYU) and Levent Alpöge (Anthropic employee), as personal research · PDE

Finite-time singularity for the Euler equations (no viscosity), a step toward Navier–Stokes. Terence Tao called it a remarkable achievement and saw no fundamental obstacle to extending the methods.

Status: Results obtained Aug 15 and Lean-checked Aug 22 by the authors’ account; papers posted publicly Sept 7

AI Weekly summary of Scientific American reporting Lilting: timeline of the dispute Terence Tao on the Euler blowup (Mathstodon)

2026-08-01

Ten advances in mathematics and theoretical computer science

Lean / IsabelleAI-ledbatch

System: Internal version of Astra (OpenAI’s next major model) · Who: OpenAI · Geometry, coding theory, group theory, operator algebras, complexity, cryptography, combinatorics

Status: Lean certificates published; manuscripts prepared by people with the model

Caveat: The problems were selected by OpenAI and the number of unsuccessful attempts was not reported.

OpenAI: Ten advances in mathematics Lean certificates: github.com/openai/ten-proofs

2026-07-20

Jacobian conjecture false for n ≥ 3

Lean / Isabellehuman–AIdisproofopen since 1939

System: Claude Fable 5 · Who: Levent Alpöge (Anthropic); his announcement credits Akhil Mathew with prompting the question · Algebraic geometry

An explicit degree-7 polynomial map of ℂ³ with Jacobian determinant −2 everywhere that sends three points to (−1/4, 0, 0). Padding with identity gives counterexamples in every dimension ≥ 3.

Status: Accepted; formalized in the Isabelle Archive of Formal Proofs; n = 2 still open

Caveat: No prompt transcript or search log has been published, so the human and AI contributions are not documented.

Isabelle AFP: Jacobian_Counterexample John D. Cook: Locally everywhere does not imply everywhere

Interactive walkthrough

2026-05

Sum–product conjecture false over the reals

expert reviewhuman, AI-inspireddisproof

System: GPT-5.5 Pro as a sounding board (it suggested one lemma); the argument is human, inspired by the unit-distance disproof · Who: Bloom, Sawin, Schildkraut, Zhelezov · Additive combinatorics

A set of real numbers whose sumset and product set both grow more slowly than the conjecture predicted, found within a week of the unit-distance result using related ideas.

Status: Preprint; the integer version remains open

Caveat: Listed as a follow-on: the argument is human-written.

arXiv:2605.28781

2026-05

Formal proof search on 353 formalized Erdős statements

Lean / Isabelleautonomousmixed

System: AlphaProof Nexus agent (Gemini 3.1 Pro + AlphaProof) · Who: Google DeepMind (Tsoukalas et al.) · Number theory, combinatorics

Status: Lean-verified

arXiv:2605.22763 Epoch AI, FrontierMath Erdős §2 (context)

2026-05-20

Erdős unit distance conjecture (#90) disproved

Lean / IsabelleAI-leddisproofopen since 1946

System: Internal OpenAI general-purpose reasoning model · Who: OpenAI · Discrete geometry

Status: Accepted; human-digested version by nine mathematicians; Sawin improved it to n^1.014 the same day

Interactive walkthrough

2026-04

Erdős #1196 (primitive sets) resolved

expert reviewAI-ledproof

System: GPT-5.4 Pro · Who: Liam Price (prompt); paper with Tao, Lichtman, Barreto and others · Number theory

From a single prompt, the model found a route unlike Erdős’s probabilistic framing that leads to a proof in under a page. Tao suggested earlier attempts may have hit a mental block.

Status: Paper with human co-authors

Caveat: The raw model output needed expert interpretation before it was usable.

arXiv:2605.00301 Physics World: AI-led solutions of Erdős problems Scientific American: An amateur just solved a 60-year-old math problem by asking AI

2026-01

Aletheia sweep of 700 open Erdős problems

expert reviewAI-ledmixed

System: Aletheia (agent on Gemini Deep Think) · Who: Google DeepMind · Number theory, combinatorics

4 novel solutions, including fully autonomous ones for #652 and #1051, and 9 problems found already solved in old literature. The #1051 solution led to a generalization paper.

Status: Published; prompts and raw responses released for the highlighted problems

Feng et al., Semi-Autonomous Mathematics Discovery with Gemini (arXiv:2601.22401)Towards Autonomous Mathematics Research (arXiv:2602.10177)

2026-01

Erdős #728 (factorial divisibility) resolved

Lean / IsabelleAI-ledproof

System: GPT-5.2 Pro; proof formalized in Lean with Harmonic’s Aristotle · Who: Kevin Barreto and Liam Price (prompting and formalization); write-up by Nat Sothanaphan · Number theory

One of the first cases where no prior solution turned up after an AI resolution. Tao described it as solved almost autonomously.

Status: Accepted on erdosproblems.com

Caveat: About ten days earlier, Barreto’s claimed first win (#333) turned out to be already implied by a 1977 Erdős–Newman paper: a reminder to search the literature first.

Sothanaphan, write-up of Aristotle’s Lean proof (arXiv:2601.07421)Tao’s wiki: AI contributions to Erdős problems Terence Tao on #728 (Mathstodon)

Benchmarks at a glance

Benchmark	What it measures	Best reported	As of
FrontierMath Tier 4 (v2, 43 problems)	Research-level problems with known answers	GPT-6 Astra 97.6%; Claude Fable 5 ≈ 88–90% (trackers differ); GPT-5.6 Sol 83% Saturated in Epoch’s sense: across all models’ attempts, every problem has now been solved at least once; no single model has a perfect score.	Sep 2026
FrontierMath: Open Problems (49)	Unsolved problems with computer-checkable answers	5 solved by AI alone and 5 by human + AI; 39 unsolved Epoch estimates 10–40% may have no solution of the required form.	Oct 2026
FrontierMath Erdős (68)	Open Erdős problems; must prove or disprove in Lean	GPT-6 Astra (pre-release) 3%; four other models 0% $300 and 72 hours per problem, one attempt each.	Sep 2026
First Proof, round 2 (10)	Unpublished research problems, refereed double-blind	7 of 10 problems got at least one passing grade across four AI systems Graded by about 30 expert referees.	Jun 2026

How to read a claim

Search the literature first: several early “AI solutions” were rediscoveries of old papers.
Prefer results with a checkable object or a formal proof; expert review is slower and scarcer.
Ask for the denominator: how many problems were tried, at what cost, with how much human steering.
A formal proof shows the theorem is true; humans still have to work out why, and how it connects to what was known.

Labels

Checked by

Lean / Isabelle: Machine-checked (Lean or Isabelle)
checkable object: Explicit object anyone can check
expert review: Checked by named experts
claimed only: Claimed; not yet independently verified

Who drove it

autonomous: Autonomous: fixed harness, no human guidance
AI-led: AI-led: people chose or prompted the problem; AI produced the argument
human–AI: Human–AI collaboration; division of labor not fully documented
human, AI-inspired: Human result built on AI-found techniques

Compiled from public sources linked on each row. The data is also available as tracker.json. Corrections welcome.