List of mathematical discoveries by artificial intelligence

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.^[10]
• In March 2026, Math Inc.'s Gauss agent formalized Maryna Viazovska's proofs of sphere packing in 8 and 24 dimensions, in approximately 200 thousand lines of Lean code.^[11][12]
• In March 2026, Google DeepMind's AlphaEvolve agent improved lower bounds for nine classical Ramsey numbers.^[13]

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.^[14] Epoch AI then used various LLMs to prove or disprove 147 of these 492 OEIS conjectures.^[15]
• In May 2026, OpenAI announced an internal model produced a disproof of the unit distance problem,^[16] and several mathematicians collaborated to produce a verification and exposition of the result.^[17]
• In May 2026, Max Grinzstajn prompted GPT-5.5 Pro to discover a counterexample for Borsuk's conjecture in dimension n = 63, the smallest dimension for which a counterexample is known.^[18][19]

Q3

More information On 1 August, OpenAI posted a proof that the unit group ...

Time period	AI provenance	Area of mathematics	Topic	Subject(s) responsible	Formal status	Source
July 2026	GPT-5.6 Sol Ultra	graph theory	proof of the cycle double cover conjecture	OpenAI	Sang-il Oum and Jim Geelen published independent expositions of the argument.[20][21]	OpenAI published an article which proved the conjecture which states that every bridgeless graph has a collection of cycles covering every edge exactly twice.[22]
July 2026	Claude Fable 5	algebraic geometry	explicit counterexample to the Jacobian conjecture, in dimension 3	Levent Alpöge and Akhil Mathew	Verified by several independent mathematicians.[23]	On 20 July, Alpöge posted on X an explicit counterexample to the Jacobian conjecture and a link to WolframAlpha which verified the counterexample.[24][23][25]
July 2026	GPT-5.6 Pro	combinatorial optimisation	counterexample to the Dinitz–Garg–Goemans conjecture	Dmitry Rybin	Counterexample published.	On 22 July, Rybin presented on X a counterexample[26][27] 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.[28]
July 2026	GPT-5.6 Sol	matrix analysis	proof of Crouzeix's conjecture	Shanmu Jin	Anne Greenbaum, Alex Townsend and Michel Crouzeix reviewed the proof and considered it to be correct.[29] An independent proof by Emiel Lorist and Felix Schwenninger, also developed with AI assistance, was published a week later.[30]	On 27 July, Jin posted a preprint proof of Crouzeix's conjecture.[31] Three days later, Alex Townsend found the preprint using GPT 5.6 and checked the proof.[29]
August 2026	unreleased version of GPT-6 Astra	group theory	construction establishing the existence of non-sofic groups	OpenAI	Lean formalization[32]	On 1 August, OpenAI posted a proof that the unit group ${\displaystyle L_{\mathbb {F} _{2}}(1,2)^{\times }}$of the binary Leavitt path algebra is non-sofic.[33]
August 2026	unreleased version of GPT-6 Astra	geometry	partial proof of Ehrhart's volume conjecture	OpenAI	Lean formalization[32]	On 1 August, OpenAI posted a proof establishing the upper bound to Ehrhart's volume conjecture, that ${\displaystyle \displaystyle \operatorname {Vol} (K)\leq {(n+1)^{n}/{n!}}}$.[33] The equality case is still open.
August 2026	unreleased version of GPT-6 Astra	complexity theory	proof of the NP-hardness of the closest vector problem	OpenAI	Lean formalization[32]	On 1 August, OpenAI posted a proof that approximating the Euclidean closest vector problem in dimension ${\displaystyle n}$ within a factor of ${\displaystyle n^{1/400}}$ is NP-hard.[33]
August 2026	OpenAI GPT-5.6 Pro[34]	complex analysis	proof of Sendov's conjecture for all degrees n ≥ 2	Lech Mazur	Lean formalization[35]	On 3 August, Mazur posted a proof of Sendov's conjecture for all degrees ${\displaystyle n\geq 2}$.[36] 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.[37][38]
August 2026	unreleased research version of Claude	analytic number theory	proven share of Riemann zeta function zeros on the critical line increased from 41.6% to 67.25%	Jarred Sumner and Anthropic	Youness Lamzouri reviewed the proof, considered it correct, and proposed a simplified proof of the result.[39][40]	On 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%.[41][42][43][44]
August 2026	unreleased version of Claude	combinatorics	Hadamard matrices constructed for the twelve orders below 2000 for which none were previously known	Levent Alpöge, Philippe Voinov and Saul Reynolds-Haertle	Computer-verified constructions[citation needed]	On 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.[45][46]
August 2026	unreleased version of Claude	Diophantine geometry	two elliptic curves with the largest known rank (at least 30 and 31, respectively)	Levent Alpöge and Ava Howell	The elliptic curves have the 30 and 31 independent basis points with infinite order listed.[47][48]	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.[49][50]
August 2026	Claude	complex manifolds	the 6-sphere admits a complex structure	Levent Alpöge	the proof has not yet been independently verified	If confirmed, this would resolve the old Hopf problem.[51]
August 2026	GPT-5.6 Sol	prime numbers	an improvement on the Erdős–Rankin conjecture (Erdős Problem 4).	DottedCalculator (pseudonym) claiming authorship of a paper uploaded to Github	Lean formalization	According to the paper, there are infinitely many gaps ${\displaystyle g_{n}=p_{n+1}-p_{n}}$ between primes such that ${\displaystyle g_{n}>{\frac {c\ \log n\ \log \log n}{\log \log \log \log n}}}$ for some constant ${\displaystyle c>0}$. 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.[52][53]
August 2026	OpenAI	prime numbers	progress on prime gaps	OpenAI	result has not yet been independently verified	Proposed a proof showing that 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.[54]
September 2026	Anthropic	percolation theory	proof of the dying percolation conjecture	Ahmed Bou-Rabee	Lean formalization[55]	The 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 proposed a 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.[56]
September 2026	Anthropic, Claude	number theory	complete computer-checked proof of Fermat's Last Theorem	Peng Tianyi	Lean formalization	Written 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.[57][58][59]
September 2026	Epoch AI, GPT-6 Astra	ring theory	disproof of the Köthe conjecture	Tom Adamczewski, Bernhard Böhmler, Rene Marczinzik	Lean formalization[60]	An exposition of the proof was posted by ring theorists Bernhard Böhmler and Rene Marczinzik.[61][62]
September 2026	Epoch AI, GPT-6 Astra	probability theory	disproof of the Ibragimov–Iosifescu conjecture for φ-mixing sequences	Tom Adamczewski	Lean formalization[63]; independent review pending	GitHub repository
September 2026	Epoch AI, GPT-6 Astra	graph theory	counterexample to an eternal domination conjecture	William Klostermeyer	?	[64]
September 2026	Epoch AI, GPT-6 Astra	combinatorics	proof of the Dittert conjecture	Tom Adamczewski	Lean formalization[65]
September 2026	Epoch AI, GPT-6 Astra	number theory	counterexample to the n = 4 case of the N conjecture	Tom Adamczewski	Lean formalization[66]	the only remaining open case

Close

Q4

More information with a deterministic algorithm that solves the 3SUM problem for integers of polynomial size in ...

Time period	AI provenance	Area of mathematics	Topic	People	Formal status	Source
October 2026	unreleased research version of Claude	complexity theory	proof of algorithms for subquadratic 3SUM and subcubic all-pairs shortest path problem	Anthropic, Josh Alman and Virginia Vassilevska Williams	Lean formalization[69]	On 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 ${\displaystyle O(n^{1.9992})}$ time and a deterministic algorithm that solves the all pairs shortest path problem for polynomial bounded integer weight in ${\displaystyle O(n^{2.9995})}$ 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.[70]

Close

On October 6, OpenAI made available 377 proofs across 722 papers over a range of mathematical topics. The proofs were generated using an unpublished model.^[71][72] Roughly 42% of the papers were published with accompanying Lean formalization.^[73] Three papers were retracted by OpenAI after peer review within three days of publication, and other papers have been criticized for making stronger claims about the problems than were formalized in Lean, or being too mathematically vague or poorly written to prove a statement.^[73]