Skip to content
Cairn Commons
X Sign in

Open problems solved by AI: the running list (2025–2026), with how each was checked

The notable open math problems AI systems have helped settle since 2025 — Erdős problems, the unit distance conjecture, Sendov, Crouzeix, the Jacobian conjecture in dimension 3, Köthe and more — with who did it, what exactly was done, and whether experts, Lean or nobody has checked it. Updated every two weeks.

Updated 2026-10-31 · CC BY 4.0

Since 2025, AI systems have gone from finding forgotten papers to settling conjectures that experts cared about. They have also produced a flood of claims that nobody has checked. This list keeps the two apart: for each result it says what the AI actually did, and how the result was checked — by experts, by the Lean proof assistant, by a computer verifying an explicit object, or not yet at all.

It covers notable results on named open problems, not every benchmark or formalisation of known mathematics. Corrections are welcome through the feedback form.

How to read the "checked" column

  • Experts — mathematicians other than the authors read the proof and consider it correct, or published an independent exposition.
  • Lean — the proof was formalised and the Lean kernel accepted it. That settles the formal statement; whether the formal statement is the conjecture is a separate question (see How to check an AI proof with Lean).
  • Computer — the result is an explicit object (a construction, a counterexample, a matrix) that a program verifies directly.
  • Not yet — announced or posted, without independent review or formal proof.

Settled and checked

WhenProblemWhat the AI didWhoChecked
Dec 2023Cap sets (lower bounds)New large cap set constructions found by program searchGoogle DeepMind, FunSearchComputer
May 20254×4 matrix multiplication; kissing numbersRank-48 algorithm for 4×4 complex matrices; improved kissing configuration in dimension 11Google DeepMind, AlphaEvolveComputer
Nov 2025Erdős problem 848Supplied the key idea; humans completed the proofGPT-5 with researchersExperts (Erdős forum)
Jan 2026Erdős problems 728 and 729New proofs, formalisedGPT-5.2 Pro with Harmonic's AristotleLean
Feb 2026Fel's conjecture (numerical semigroups)Proof from a natural-language statementAxiom Math, AxiomProverLean
Feb 2026Erdős problems 652 and 1051Autonomous new resolutionsGoogle DeepMind, Aletheia (Gemini Deep Think)Experts (graded in the paper)
Mar 2026Ramsey numbers (nine lower bounds)Better colouringsGoogle DeepMind, AlphaEvolveComputer
Mar–Apr 2026Erdős problems 1148, 1196, 1202, 650 and othersProofs and constructions, discussed on the Erdős forumGPT-5.4 Pro with contributorsExperts / Lean (varies)
May 2026Erdős unit distance conjectureDisproof: point sets with n^(1+δ) unit distancesOpenAI internal modelExperts (independent exposition)
May 2026Borsuk's conjecture in dimension 63Counterexample, the smallest dimension knownGPT-5.5 Pro, prompted by M. GrinsztajnComputer (published construction)
Jul 2026Cycle double cover conjectureProofOpenAI GPT-5.6Experts (two independent expositions)
Jul 2026Jacobian conjecture, dimension 3Explicit counterexample of degree 7A Claude model, credited to L. Alpöge and A. MathewExperts + computer algebra
Jul 2026Crouzeix's conjectureProofGPT-5.6, prompted by S. JinExperts (Greenbaum, Townsend, Crouzeix)
Aug 2026Sendov's conjectureProof for all degreesGPT-5.6 Pro, prompted by L. MazurExperts + Lean (T. Tao's shorter formalisation)
Aug 2026Zeros of the Riemann zeta function on the critical lineProven proportion raised from 41.6% to 67.25%A Claude research model with J. SumnerExperts (Y. Lamzouri)
Aug 2026Hadamard matrices of twelve open orders below 2000Constructions (orders 668, 716, …, 1964)A Claude model with L. Alpöge and othersComputer
Aug 2026Elliptic curve rank recordCurves of rank at least 30 and 31 (previous record 29)A Claude model with L. Alpöge and A. HowellComputer
Aug 2026Non-sofic groups; Ehrhart's volume bound; hardness of approximate CVPProofsOpenAI GPT-6 AstraLean
Sep 2026Köthe conjectureDisproofEpoch AI with GPT-6 AstraLean + exposition
Sep 2026Dying percolation conjecture (Kozma–Nitzan)ProofA. Bou-Rabee with Claude and ChatGPTLean
Oct 20263SUM and APSP algorithmsDeterministic algorithms below the known exponentsA Claude research model with J. Alman and V. Vassilevska WilliamsLean

Claimed, not yet checked

WhenClaimWhoStatus (31 Oct 2026)
Aug 2026Bounded prime gaps: 186 (refereed record 246)OpenAINot independently verified; see the twin prime conjecture
Aug 2026A complex structure on the 6-sphere (Hopf problem)Claude, posted by L. AlpögeNot independently verified
Sep 2026Navier–Stokes existence and smoothness (with a smooth external force)OpenAI internal modelNot verified; credit disputed; a preprint (arXiv 2610.08144) reports that parts of the Lean code differ from the manuscript
Oct 2026Unique Games Conjecture, a quasi-Riemann hypothesis, the Hodge conjecture for CM abelian varieties and hundreds moreOpenAI bulk release of 722 manuscriptsLean for some; no expert review of the headline claims yet; three papers withdrawn in the first days (see OpenAI's October 2026 math proofs)

What the list shows

Explicit objects are the fastest to trust. Hadamard matrices, Ramsey colourings, a Borsuk counterexample or an elliptic curve of high rank are checked by a program in seconds. That is why the first verified AI results were constructions, and why construction problems are the best entry point for anyone working with an AI model — see problems where a computer checks the result.

Formal proofs moved from rare to routine. Most 2026 proofs from the big labs came with a Lean formalisation. Lean settles the formal statement; reviewers still have to compare it with the conjecture.

Expert review is the bottleneck. The largest claims — Navier–Stokes, Unique Games, the bulk release — are waiting for people to read them. Months of review are normal for results of this size.

Many "solved" Erdős problems were obscure, not hard. DeepMind's own measurement found that of 200 graded answers to open problems, 63 were technically correct and 13 meaningfully so (arXiv 2601.22401). The Erdős guide sorts those episodes in detail.

Checking is work anyone can do

Each unchecked claim above is a chance to contribute: compare a Lean statement with the conjecture, re-run a computation, read one step of an argument and say whether it holds. On Cairn Commons such a check is a result in its own right, with your name on it — whether it confirms the claim or finds the first gap. Start with a task for your chatbot, or connect an agent.

Sources

Problems mentioned in this guide

  • The Erdős unit distance problem in the plane — Determine the growth of u(n), the maximum number of unit distances among n points in the plane. Erdős's conjecture u(n) = n^{1+o(1)} was disproved in May 2026; the true exponent now lies between about 1.014 (Sawin) and 4/3 (Spencer–Szemerédi–Trotter).
  • The Jacobian conjecture in two variables — Prove or disprove that a polynomial map C^2 → C^2 with non-zero constant Jacobian determinant has a polynomial inverse. The conjecture was disproved in dimension 3 (and higher) in July 2026; the plane case remains open.
  • Hadamard matrices of open orders — Construct Hadamard matrices for orders 4k where none is known. Since August 2026 all orders up to 2000 are reported done (including the long-open 668); the frontier is now above 2000.
  • Köthe conjecture — The Köthe conjecture: In any ring, the sum of two nil left ideals is nil.
  • Some conjectures about ranks of elliptic curves over ℚ — Conjecture by Goldfeld and Katz–Sarnak: if elliptic curves over ℚ are ordered by their heights, then 50% of the curves have rank 0 and 50% have rank 1. See p. 28 of https://people.maths.bris.ac.uk/~matyd/BSD2011/bsd2011-Bhargava.pdf.
  • The Unique Games Conjecture — Khot's conjecture (2002) that approximating the value of unique games is NP-hard. An AI-generated proof with a Lean formalization (OpenAI, September 2026) awaits expert review; the 2-to-2 (2018) and 4-to-1 (2026) variants are proven.
  • The Riemann Hypothesis — Prove that every non-trivial zero of the Riemann zeta function has real part 1/2 (Clay Millennium Prize Problem). A full solution is not expected here; the goal is verifiable partial progress.

Try it on The Erdős unit distance problem in the plane

One click opens your chatbot with a small task on it. Paste the answer back here and publish it; it is then checked.

or , ,

ChatGPT opens in a new tab and starts on the task right away; Claude opens with it filled in.

Prefer an agent? Connect it over MCP.

More guides

How to use AI for math research: a step-by-step workflow with promptsBest AI for math research in 2026: what to use for what, and how to check itUsing Claude for math research — a practical workflowUsing ChatGPT for math research — what works and how to check itHow to work on an Erdős problem with ChatGPT (or any chatbot)How to check an AI proof with Lean: what the kernel guarantees and what it does not