Beginning in the mid-2020s, large language models, including reasoning models, have made increasing progress in generating mathematical proofs at research level. Most such proofs have been conducted using models from OpenAI and Anthropic. This is a list of notable discoveries conducted primarily by such models.

The degree of human intervention in AI-generated mathematical proofs may vary and remain unclear. Subjects responsible for publishing such proofs, including individuals and AI companies such as OpenAI, often fail to disclose used prompts, structure of pipelines used as a model workflow, or specific models used for generating proofs. The publication of such proofs may not satisfy standards of science articles. It may not have passed independent review or peer review, and instead be published on corporate websites, personal websites, or social media.

2023

In December 2023, researchers at Google DeepMind used a pre-trained LLM to discover a new lower bound for the cap set problem and new algorithms for the bin packing problem. The results for the cap set problem were verified by mathematician Jordan Ellenberg.

2024

In October 2024, researchers at Meta and the Ecole des Ponts et Chaussees found pre-trained Seq2seq transformers could discover new global Lyapunov functions at a higher rate than non-AI systems.

2025

In May 2025, Google DeepMind's AlphaEvolve agent discovered an optimization for the Strassen algorithm, reducing the scalar multiplications needed for 4x4 matrices from 49 to 48. It also improved the lower bounds for 11 kissing numbers. In September 2025, Math Inc.'s Gauss agent formalized the strong prime number theorem in Lean, producing ~25,000 lines of code and formally proving >1,000 theorems. In November 2025, researchers at Chinese universities constructed a reinforcement learning algorithm which improved the lower and upper bounds for 15 kissing numbers.

2026

Q1

In February 2026, Google DeepMind used its Gemini model to survey the 700 open Erdős problems, which proved four of them and found nine unknown published solutions. In March 2026, Math Inc.'s Gauss agent formalized Maryna Viazovska's proofs of sphere packing in 8 and 24 dimensions, in ~200 thousand lines of Lean code. In March 2026, Google DeepMind's AlphaEvolve agent improved lower bounds for nine classical Ramsey numbers.

Q2

In May 2026, Google DeepMind used an AlphaEvolve-like model, adapted for mathematical proofs, to prove nine Erdős problems and 44 out of 492 formalized OEIS conjectures. Epoch AI then used various LLMs to prove/disprove 147 of these 492 OEIS conjectures. In May 2026, OpenAI announced an internal model produced a disproof of the unit distance problem, and several mathematicians collaborated to produce a verification and exposition of the result. In May 2026, Max Grinzstajn prompted GPT-5.5 Pro to discover a counterexample for Borsuk's conjecture in dimension , the smallest dimension for which a counterexample is known.

Q3 Time periodAI provenanceArea of mathematicsTopicPeopleFormal statusSourceJuly 2026GPT-5.6 Sol Ultragraph theoryproof of the cycle double cover conjectureOpenAISang-il Oum and Jim Geelen published independent expositions of the argument.OpenAI published an article which proved the conjecture which states that every bridgeless graph has a collection of cycles covering every edge exactly twice.July 2026Claude Fable 5algebraic geometryexplicit counterexample to the Jacobian conjecture, in dimension 3Levent Alpöge and Akhil MathewVerified by several independent mathematicians.On 20 July, Alpöge posted on X an explicit counterexample to the Jacobian conjecture and a link to WolframAlpha which verified the counterexample.July 2026GPT-5.6 Procombinatorial optimisationcounterexample to the Dinitz–Garg–Goemans conjectureDmitry RybinCounterexample published.On 22 July, Rybin presented on X a counterexample in which a fractional flow of 58 exists, yet every unsplittable flow that meets the capacity bound costs at least 60. The disproof establishes that the theorem's capacity guarantee and a matching cost guarantee cannot always be achieved simultaneously by a single flow.July 2026GPT-5.6 Solmatrix analysisproof of Crouzeix's conjectureShanmu JinAnne Greenbaum, Alex Townsend and Michel Crouzeix reviewed the proof and considered it to be correct. An independent proof by Emiel Lorist and Felix Schwenninger, also developed with AI assistance, was published a week later.On 27 July, Jin posted a preprint claiming a proof of Crouzeix's conjecture. Three days later, Alex Townsend found the preprint using GPT 5.6 and checked the proof.August 2026unreleased version of GPT-6 Astragroup theoryconstruction establishing the existence of non-sofic groupsOpenAILean formalizationOn 1 August, OpenAI posted a proof that the unit group of the binary Leavitt path algebra is non-sofic.August 2026unreleased version of GPT-6 Astrageometrypartial proof of Ehrhart's volume conjectureOpenAILean formalizationOn 1 August, OpenAI posted a proof establishing the upper bound to Ehrhart's volume conjecture, that . The equality case is still open.August 2026unreleased version of GPT-6 Astracomplexity theoryproof of the NP-hardness of the closest vector problemOpenAILean formalizationOn 1 August, OpenAI posted a proof that approximating the Euclidean closest vector problem in dimension within a factor of is NP-hard.August 2026OpenAI GPT-5.6 Procomplex analysisproof of Sendov's conjecture for all degrees Lech MazurLean formalization On 3 August, Mazur posted a paper on X claiming a proof of Sendov's conjecture for all degrees . Terence Tao examined and streamlined the argument, produced a separate and shorter Lean formalization, and noted the proof also established the stronger Phelps–Rodriguez conjecture.August 2026unreleased research version of Claudeanalytic number theoryproven share of Riemann zeta function zeros on the critical line increased from 41.6% to 67.25%Jarred Sumner and AnthropicLean formalizationOn 10 August, Anthropic announced that it had made progress on increasing the bound for the fraction of zeroes of the Riemann zeta function from 41.6% to 67.25%.August 2026unreleased version of ClaudecombinatoricsHadamard matrices constructed for the twelve orders below 2000 for which none were previously knownLevent Alpöge, Philippe Voinov and Saul Reynolds-Haertle Computer-verified constructionsOn 12 August, Alpöge posted constructions for Hadamard matrices for twelve unresolved orders: 668, 716, 892, 1132, 1244, 1388, 1436, 1676, 1772, 1916, 1948 and 1964. The smallest of those, 668, had been the smallest open case of the Hadamard conjecture since 2005. The conjecture itself, which concerns all orders divisible by four, remains open.August 2026unreleased version of ClaudeDiophantine geometrytwo elliptic curves with the largest known rank (at least 30 and 31, respectively)Levent Alpöge and Ava HowellThe elliptic curves have the 30 and 31 independent basis points with infinite order listed.On 20 August, an elliptic curve of rank at least 30 was posted to the Elliptic Curve Rank Leaderboard, with the solution credited to Alpöge and Howell. On 23 August, an elliptic curve of rank at least 31 was posted. These curves broke the previous known record of rank at least 29.August 2026Claudecomplex manifoldsthe 6-sphere admits a complex structureLevent Alpögethe claim has not yet been independently verifiedIf confirmed, this would resolve the old Hopf problem.August 2026GPT-5.6 Solprime numbersan improvement on the Erdős–Rankin conjecture (Erdős Problem 4).DottedCalculator (pseudonym) claiming authorship of a paper by uploaded a paper to GithubLean formalizationAccording to the paper, there are infinitely many gaps between primes such that for some constant . This improves on the original proof of the conjecture by Ford, Green, Konyagin, Maynard and Tao from 2014. According to Green, the new result uses a new but relatively elementary approach that would have been strong enough to independently solve the original problem without their 2014 paper, but which could have been discovered in the 1960s.August 2026OpenAIprime numbersprogress on prime gaps?result has not yet been independently verifiedClaim to have proved there are infinitely many prime numbers that are at most 186 apart, an improvement on the previous bound of 246 that was established in 2014 by the Polymath Project. The OpenAI r.September 2026Anthropicpercolation theoryproof of the dying percolation conjectureAhmed Bou-RabeeLean formalizationThe result was obtained by proving an equivalent conjecture by Gady Kozma and Shaha Nitzan. Building on the result, Ahmed Bou-Rabee from the University of Pennsylvania published a claimed proof of the remaining Kozma-Nitzan conjectures, which he found the following day with ChatGPT Sol 5.6 Ultra and formalized in Lean with Claude Fable 5.1.September 2026Anthropic, Claudenumber theorycomplete computer-checked proof of Fermat's Last TheoremPeng TianyiLean formalizationWritten over 11 days. It formalizes a simplified version of the original proof found by Andrew Wiles in 1994. Work on formalizing the theorem had started early in the century. The proof in Lean is 13 million lines long, the largest Lean proof written to date, and 29,500 theorems were formally proved for this task.September 2026Epoch AI, GPT-6 Astraring theorydisproof of the Köthe conjectureTom Adamczewski, Bernhard Böhmler, Rene Marczinzik Lean formalizationAn exposition of the proof was posted by ring theorists Bernhard Böhmler and Rene Marczinzik.September 2026Epoch AI, GPT-6 Astraprobability theorydisproof of the Ibragimov–Iosifescu conjecture for φ-mixing sequencesTom AdamczewskiLean formalization; independent review pendingGitHub repositorySeptember 2026Epoch AI, GPT-6 Astragraph theorycounterexample to an eternal domination conjectureWilliam Klostermeyer?September 2026Epoch AI, GPT-6 Astracombinatoricsproof of the Dittert conjectureTom AdamczewskiLean formalizationSeptember 2026Epoch AI, GPT-6 Astranumber theorycounterexample to the case of the N conjecture Tom AdamczewskiLean formalizationthe only remaining open case

Navier–Stokes equations

In September 2026, OpenAI claimed an internal model more powerful than GPT-6 Astra had solved the Navier–Stokes existence and smoothness problem, one of the Millennium Prize Problems. The claim has not been verified by the wider mathematical community. The credit for the discovery is disputed.

Q4

Time periodAI provenanceArea of mathematicsTopicPeopleFormal statusSourceOctober 2026unreleased research version of Claudecomplexity theoryproof of algorithms for subquadratic 3SUM and subcubic all-pairs shortest path problemAnthropic, Josh Alman and Virginia Vassilevska WilliamsLean formalizationOn 5 October, Josh Alman and Virginia Vassilevska Williams published a preprint on ArXiv with a deterministic algorithm that solves the 3SUM problem for integers of polynomial size in time and a deterministic algorithm that solves the all pairs shortest path problem for polynomial bounded integer weight in time. The authors stated that Anthropic's internal research model discovered the result, formalized it in Lean and shared it with them to assist them with writing the paper.

See also Automated theorem proving Computer-assisted proof Leiden Declaration on Artificial Intelligence and Mathematics Mathematics and artificial intelligence

References

External links VibeMathed: Repository of AI solutions to open mathematics problems