There’s a new genre of AI headline that would’ve sounded absurd 18 months ago: AI solved an open math problem.
Now we’ve got enough examples that the harder question isn’t whether it’s happening. It’s how to separate the real thing from the hype. Some of the splashiest “AI solved math” claims this year turned out to be rediscoveries, literature misses, or proofs of AI contributions to Erdős problems. But a smaller set has held up well enough to matter, and that’s the set worth tracking.
What’s changed is the workflow. Models are now generating proof ideas, turning them into formal proofs in Lean, and sometimes doing it end-to-end on problems that were still open when the model started.
That doesn’t mean we’ve automated Terence Tao. It does mean AI is moving from “fast tutor” territory into something more uncomfortable for mathematicians and more interesting for everyone else: genuine research contribution.
That shift is especially visible in the Erdős ecosystem, where public discussion has become unusually transparent, and in the recent run of Axiom Math results, which keep pushing formalized proof deeper into real research terrain. We’ve also seen the “under review” bucket grow, including OpenAI’s First Proof work and the GPT-5.4 Pro claims now circulating around FrontierMath and X.
If you want the clean version, here it is: a list of the strongest publicly documented cases as of March 11, 2026, plus the credible claims that still need more sunlight. (Writers note: I hope to update this with time. If you know of any verified problems or see any errors, please reach out and we will look into getting them added. It's important to me this list be accurate.)
Verified AI Mathematics Solutions
Erdős Problem #848
Brief description: A number theory problem about how large a set of positive integers can be if, for every pair in the set, the value of their product plus 1 always has a prime factor appearing to an even power. OpenAI says GPT-5 supplied the key idea that helped complete the proof.
Date solved or verified: November 20, 2025
Company / model: OpenAI / GPT-5
What does this finding unlock? This settles a specific extremal question in multiplicative number theory, so its main value is closing a well-known loose end cleanly. The likely payoff is methodological: mathematicians can now test whether the same structure extends to related “product-plus-constant” and prime-factor constraints.
Erdős Problem #728
Brief description: A divisibility problem asking whether infinitely many triples exist with a specific logarithmic gap inside a factorial divisibility pattern. The public paper presents this as a fully autonomous AI resolution, with formal verification in Lean.
Date solved or verified: January 12, 2026
Company / model: OpenAI + Harmonic / GPT-5.2 Pro + Aristotle
What does this finding unlock? This appears to open up new technique around factorial divisibility and logarithmic gap control, which could matter for nearby problems in elementary number theory. It probably won’t instantly unlock a whole field, but it gives researchers a new proof pattern to try on similar divisibility questions.
Erdős Problem #729
Brief description: Another open Erdős problem that the public Erdős forum records as a fully AI-generated resolution, later autoformalized from proof notes and TeX into Lean. It’s treated as a genuine new solve pending no prior-literature surprise.
Date solved or verified: January 10, 2026
Company / model: OpenAI + Harmonic / GPT-5.2 Pro + Aristotle
What does this finding unlock? This is best framed as progress inside the broader Erdős ecosystem rather than a dramatic field-wide unblock. Its main mathematical value is likely that the argument or formalization strategy can be adapted to adjacent combinatorial or additive problems.
Fel’s Conjecture on Syzygies of Numerical Semigroups
Brief description: A conjecture in algebra about explicit formulas for certain alternating syzygy power sums in numerical semigroups. Axiom says AxiomProver produced the proof automatically from a natural-language statement and formalized it in Lean.
Date solved or verified: February 3, 2026
Company / model: Axiom Math / AxiomProver
What does this finding unlock? This gives researchers an explicit formula linking syzygy power sums to gap data and symmetric-polynomial structure, which should make certain invariants easier to compute and compare. That matters because numerical semigroups sit close to questions in commutative algebra and singularity theory, where explicit formulas are genuinely useful.
Conjecture A.10 in Parity of k-differentials in genus zero and one
Brief description: A missing number-theoretic hypothesis needed to turn a previously conditional algebraic-geometry result into an unconditional one. AxiomProver proved the missing piece by reducing it to tractable symbolic ingredients.
Date solved or verified: February 3, 2026
Company / model: Axiom Math / AxiomProver
What does this finding unlock? This one really does unblock something: it removes the missing hypothesis that had kept a parity result conditional. The immediate payoff is that mathematicians can now use that theorem unconditionally in follow-on work on moduli spaces and the geometry of differentials.
“Almost all primes are partially regular”
Brief description: A new theorem in algebraic number theory showing that a density-one subset of primes satisfies a partial regularity condition tied to Bernoulli numbers, class groups, and partial Vandiver-style phenomena. The paper says the theorem was generated by AxiomProver from a natural-language conjecture and formalized in Lean.
Date solved or verified: February 4, 2026
Company / model: Axiom Math / AxiomProver
What does this finding unlock? This has the strongest downstream consequences of the bunch. The paper ties it to a partial Vandiver theorem and to consequences for p-adic L-functions, congruences between cusp forms and Eisenstein series, and p-torsion in algebraic K-groups, so this is the clearest case where solving the problem feeds directly into other active areas.
Erdős Problem #652
Brief description: Google DeepMind’s Aletheia paper lists this as one of its autonomous novel Erdős resolutions. The claim appears in a serious paper, though the public summaries are less friendly than the OpenAI and Axiom examples.
Date solved or verified: February 5, 2026
Company / model: Google DeepMind / Gemini Deep Think via Aletheia
What does this finding unlock? Even if it’s less narratively tidy, it matters because it shows more than one lab is now producing plausible new math. That makes this look like a category shift, not a company-specific stunt.
Erdős Problem #1051
Brief description: Also listed in the Aletheia paper as a novel autonomous Erdős resolution. Publicly available summaries are sparse, but the paper treats it as another bona fide new result rather than a rediscovery.
Date solved or verified: February 5, 2026
Company / model: Google DeepMind / Gemini Deep Think via Aletheia
What does this finding unlock? The bigger signal here is portfolio, not headline value. Once a system can credibly produce multiple new results, the conversation shifts from “can AI do math research?” to “how often, and in what fields?”
That Axiom run is especially worth watching. As we wrote in our earlier piece on Axiom’s autonomous theorem proving, the most interesting part isn’t that the model got one proof right. It’s that the loop is tightening: conjecture, prove, formalize, learn, repeat.
And if you want the founder-level version of that story, our interview with Carina Hong is still one of the best windows into how this category is being built. At the time, the pitch sounded almost too ambitious. Then the results started landing.
Small prime factors of (nk)(kn)
Brief description: This resolves an Erdős question about the small-prime divisor structure of binomial coefficients. The new paper presents a short proof found entirely by an internal OpenAI model.
Date solved or verified: March 31, 2026
Company / model: OpenAI / internal model
What does this finding unlock? This gives number theorists a new short argument for controlling prime divisors of binomial coefficients, an area where Erdős posed many related problems. The next step is to test whether the same idea extends to nearby questions about divisor sizes and prime-factor distributions in combinatorial quantities.
Splitting additive bases into two bounded-gap pieces
Brief description: This answers an Erdős question asking whether an additive basis can always be split into two pieces A1A1 and A2A2 so that each self-sumset Ai+AiAi+Ai has bounded gaps. The proof appears in the same new OpenAI-assisted paper.
Date solved or verified: March 31, 2026
Company / model: OpenAI / internal model
What does this finding unlock? This gives a new structural theorem about additive bases, showing they can be decomposed more cleanly than was previously known. Mathematicians can now ask whether similar splitting principles hold in stronger additive settings or help on nearby Erdős-Turán-style problems.
Hlawka-Petersen well-distribution of {αp}{αp}
Brief description: This settles an Erdős-raised question about whether the fractional parts {αp}{αp}, with pp prime, are “well-distributed” in the sense introduced by Hlawka and Petersen. It is the third result in the new OpenAI paper.
Date solved or verified: March 31, 2026
Company / model: OpenAI / internal model
What does this finding unlock? This closes off one more longstanding distribution question about primes under irrational rotation. The next mathematical step is to see whether the method can be pushed to stronger equidistribution statements or adapted to other prime-generated sequences.
A Ramsey-style Problem on Hypergraphs
Brief description: Epoch AI now marks this FrontierMath open problem as solved. The task was to improve lower bounds on a hypergraph quantity H(n)H(n) by constructing larger hypergraphs with no large partitions, and the first accepted solution was elicited with GPT-5.4 Pro.
Date solved or verified: March 23, 2026
Company / model: OpenAI / GPT-5.4 Pro
What does this finding unlock? The solution improves the known lower-bound construction for H(n)H(n), which is a real combinatorics advance rather than just a benchmark win. The obvious next step is to generalize the construction and understand why the improved lower bound lines up so well with the upper-bound side of the problem.
Erdős Problem #1148
Brief description: A number theory problem asking whether every sufficiently large integer can be written as n=x2+y2−z2n=x2+y2−z2 with all three squares bounded by nn. The Erdős Problems tracker now marks it proved and Lean-verified, crediting Chojecki and GPT-5.4 Pro for a proof using a form of Duke’s theorem from Einsiedler, Lindenstrauss, Michel, and Venkatesh.
Date solved or verified: March 23, 2026
Company / model: OpenAI / GPT-5.4 Pro
What does this finding unlock? This closes a clean bounded-representation problem by connecting it to deep equidistribution machinery for quadratic forms. The main value is not just the answer, but the proof pattern: AI helped spot a route from an elementary-looking ternary quadratic question into a powerful existing theorem.
Erdős Problem #1202
Brief description: A sieve-theoretic question about whether choosing half the congruence classes modulo enough small primes can force almost all integers up to nn to be eliminated. Price and GPT-5.4 Pro resolved it in the negative with a construction leaving a linearly large surviving set.
Date solved or verified: April 7-12, 2026
Company / model: OpenAI / GPT-5.4 Pro
What does this finding unlock? This is a real additive/analytic number theory counterexample, and it also matters because the problem appears as Problem 44 on Ben Green’s open problems list. It gives researchers a sharper sense of where large-sieve intuition stops being enough.
Erdős Problem #1196
Brief description: A conjecture of Erdős, Sárközy, and Szemerédi on primitive sets, asking for the sharp asymptotic upper bound on ∑a∈A1/(aloga)∑a∈A1/(aloga) when all elements of AA are large. The Erdős Problems tracker now says GPT-5.4 Pro, prompted by Liam Price, solved it by proving the required 1+O(1/logx)1+O(1/logx) bound.
Date solved or verified: April 15, 2026
Company / model: OpenAI / GPT-5.4 Pro
What does this finding unlock? This is one of the stronger new additions because it improves a known partial bound and lands directly in the theory of primitive sets. It also shows the Erdős tracker moving from “interesting claim” territory into a recorded solved status after mathematical discussion.
Erdős Problem #258
Brief description: An irrationality problem asking whether ∑nτ(n)/(a1⋯an)∑nτ(n)/(a1⋯an) is irrational for every positive integer sequence an→∞an→∞. Chojecki and GPT-5.4 Pro answered it affirmatively, using recent work of Tao and Teräväinen.
Date solved or verified: April 15, 2026
Company / model: OpenAI / GPT-5.4 Pro
What does this finding unlock? This extends earlier special cases, including the monotone-sequence case, to the full generality Erdős asked for. Its broader value is another example of AI helping locate the right modern theorem to collapse an old irrationality problem.
Erdős Problem #650
Brief description: A number theory problem asking for the exact value of f(m)f(m), where f(m)f(m) measures how many distinct divisible representatives must appear in every interval of length 2N2N, given an mm-element set A⊆{1,…,N}A⊆{1,…,N}. GPT-5.4 Pro first proved the upper bound f(m)≤⌈2m⌉f(m)≤⌈2m⌉, and GPT-5.4 Pro plus Aristotle contributed the matching lower-bound argument, later written up in cleaned human form. Part of the upper-bound story was already known from Erdős and Selfridge, but the exact formula now recorded is new: f(m)=min(m,⌈2m⌉)f(m)=min(m,⌈2m⌉).
Date solved or verified: March 30-April 2, 2026
Company / model: OpenAI + Harmonic / GPT-5.4 Pro + Aristotle
What does this finding unlock? This pins down the exact behavior of f(m)f(m), not just its order of growth, which is why the result deserves to move out of the messy “under review” bucket. It is also a useful reminder that AI math credit will often be hybrid: the model found or sharpened key pieces, formalization helped close a gap, and humans then cleaned the proof into the final mathematical record.
Meaningful AI Proof Contributions
Erdős Problem #1026
Brief description: A problem in extremal algebra asking whether a finite set of nonzero real numbers must satisfy a sharp lower bound on the size of its sum-product set. In late 2025, mathematicians working with Aristotle produced a formalized proof of the main conjecture, and Terence Tao later described the episode as a real human-AI collaboration. While the core result appears to have existed in prior literature, that wasn't known at the time. Now, meaning this is better understood as a meaningful AI proof contribution than a clean new solution to a still-open problem. Still, it was a highly meaningful first step.
Date solved or verified: December 8, 2025
Company / model: Harmonic / Aristotle
What does this finding unlock? This milestone helped formalize, verify, and accelerate real mathematical reasoning. Cases like this suggest AI may become genuinely useful not just for generating new conjectures or proof sketches, but for turning partial arguments into rigorous, checkable mathematics faster than traditional methods ever have.
Erdős Problem #1217
Brief description: A problem of Erdős, Sárközy, and Szemerédi about finding an infinite divisibility chain inside a sequence with positive lower logarithmic density, with the chain matching a weighted logarithmic-density lower bound. The tracker now marks the problem proved, while the discussion records a GPT-5.4 Pro solution prompted and checked by Quanyu Tang and Yanyang Li, alongside an independently forthcoming human writeup.
Date solved or verified: April 15-16, 2026
Company / model: OpenAI / GPT-5.4 Pro
What does this finding unlock? I’d place this slightly more cautiously than #1196, because the GPT-specific contribution is still mainly documented in the discussion rather than the main problem note. Still, it looks like a serious AI-assisted proof contribution in the same primitive-set/divisibility-chain neighborhood as #1196.
On infinite sets with no 3 on a line
Brief description: This paper gave a new AI-generated construction answering a question of Erdős, Nešetřil, and Rödl in combinatorial geometry. But the authors note that after sharing the proof, Vojtěch Rödl pointed out the result can already be deduced from earlier work.
Date solved or verified: February 24, 2026
Company / model: OpenAI / internal model
What does this finding unlock? Even if it is not a clean new solve, it shows AI can produce short, intelligible constructions in active combinatorics. That matters because simpler proofs and constructions can still generate follow-on questions and cleaner ways of organizing a field.
Credible, But Under Review
OpenAI First Proof submissions
Brief description: OpenAI says at least five submissions, on Problems 4, 5, 6, 9, and 10, have a high chance of being correct, with several others still under review. These are serious research-level benchmark problems, but they should stay in the provisional bucket until expert review closes.
Date solved or verified: February 20, 2026 and the First Proof paper
Company / model: OpenAI / unreleased research-time system used for First Proof submissions
What does this finding unlock? If these results clear review, they would widen the field fast because they point to multiple potential solves rather than one flagship example. For now, the right framing is momentum, not certainty.
GPT-5.4 Pro on FrontierMath’s “small” Diophantine equations
Brief description: Epoch AI’s open problem page says GPT-5.4 Pro solved two of the nine open equations in a finiteness problem for low-size Diophantine equations via direct substitution. The page still marks the overall problem as unsolved, so this currently looks like a real partial advance, not a full closure.
Date solved or verified: March 5, 2026
Company / model: OpenAI / GPT-5.4 Pro
What does this finding unlock? Partial progress on curated open-problem sets is still important because it shows models can chip away at live research questions rather than only answer benchmark leftovers. It also hints that automatically checkable math may become one of the first domains where AI can post a steady stream of incremental discoveries.
Erdős Problem #650
Brief description: The Erdős AI-contributions wiki says AI produced a full solution stronger than the literature, but the original problem itself was already solved in prior human work. That makes it interesting and useful, but not a clean “AI solved an open problem” case.
Date solved or verified: current Erdős AI contributions tracker
Company / model: OpenAI / GPT-5.4 Pro
What does this finding unlock? This is a good example of why the category is messy. AI may already be strong enough to produce mathematically valuable results even when the headline claim turns out to be historically wrong. So, the AI-generated argument may still be stronger or cleaner than the known literature, which still matters.
Gaussian Correlation Inequality: Optimal Extensions
Brief description: SolveAll discussion indicates GPT-5.4 Pro produced a solution to a post-Royen Gaussian correlation extension problem, and Edgar Dobriban wrote that he had double-checked it and it “seems to be correct.” But the public page is still a bit messy, so I would not move it into the fully verified bucket yet.
Date solved or verified: March 2026 discussion on SolveAll
Company / model: OpenAI / GPT-5.4 Pro
What does this finding unlock? If correct, this would clarify the real boundary of how far Gaussian-correlation-type inequalities extend beyond the centered case. That matters for convex geometry, Gaussian probability, and the multivariate-normal inequalities that sit downstream of this line of work.
Why AI Math Solutions Are A Bit Messy
That’s really the story here. AI math progress is no longer speculative. But the scorecard is messy because mathematics has memory. A model can produce a valid proof and still not deserve credit for a “new” result if someone quietly solved it in 1966.
So the right lens is not “did AI solve all the unsolved math?” Obviously not.
It’s whether AI has crossed the line into contributing novel, defensible results in active research workflows. On that question, the answer now looks increasingly like yes.
And once you combine that with formal verification, public trackers, and labs racing to turn theorem-proving into infrastructure, you get something bigger than a few flashy papers. You get the early shape of a new research stack, where mathematicians stop using AI as autocomplete and start using it as a collaborator, critic, and sometimes first draft of the proof itself.
With any luck, Hong's stated goal of mathematical superintelligence may well make a massive impact. Watch their work, as well as what the frontier labs are doing, so you don't miss watching milestones as they fall.
That doesn’t make human mathematicians obsolete, even if we all get our own Terence Tao in our pocket.
It probably makes high-level taste, problem selection, and proof judgment more valuable. But it does mean the old comfort line, “AI can imitate math but not do math,” is getting harder to say with a straight face.
--
If you haven't, please subscribe to The Neuron daily AI newsletter and our podcast. We'd love to count you as one of our readers.
