What AI has
actually discovered

Counterexample to the Dinitz–Garg–Goemans conjecture#

An explicit seven-node network whose cheapest single-route (unsplittable) shipping costs more than its fractional cost even under the allowed capacity slack, disproving a conjecture from the late 1990s.

Dinitz, Garg, and Goemans proved that any fractional multicommodity flow can be rounded to an unsplittable (single-path-per-demand) flow while violating each arc's capacity by at most the maximum demand. Goemans conjectured this rounding could also be done without increasing the total cost. The counterexample is a directed graph on seven nodes carrying three demands (15, 10, 15); its fractional solution costs 58, yet every unsplittable routing that stays within the allowed capacity cushion (violation ≤ 15) costs at least 60. Rybin reached it with GPT-5.6 Pro in four short prompts and reported that the model returned proof certificates, an exhaustive-enumeration verification program, machine-readable data, and LaTeX source.

WithDmitry Rybin

Counterexamples to the Gaussian moments conjecture#

Explicit low-degree polynomials disproving a 2017 conjecture that had been proposed as a route to proving the Jacobian conjecture, found days after that conjecture was itself disproved.

Derksen, van den Essen and Zhao proposed the Gaussian moments conjecture and showed that the Jacobian conjecture would follow from it. Long reports that a cubic counterexample in four variables was produced by GPT-5.6 Sol Pro with no human intervention after the initial prompt, which simply noted that the Jacobian conjecture had just been disproved and asked whether a small counterexample to GMC might therefore exist; Claude Fable 5 then found a quartic counterexample in three variables and supplied independent algebraic checks. Together these show GMC(n) is false for every n ≥ 3.

WithChristopher D. Long

Counterexample to the Jacobian conjecture in dimension three#

An explicit polynomial map in three variables with constant Jacobian determinant −2 that is nevertheless not invertible, disproving a conjecture open since 1939.

The map F(x,y,z) = (u³z + y²u(4+3xy), y + 3xu²z + 3xy²(4+3xy), 2x − 3x²y − x³z) with u = 1+xy has Jacobian determinant identically −2, yet sends the three distinct points (0,0,−¼), (1,−3/2,13/2) and (−1,3/2,13/2) all to (−¼,0,0). A map with a global inverse cannot be three-to-one. Alpöge, a number theorist at Anthropic, announced it on X the day it was found.

WithLevent Alpöge

Near-quadratic lower bound for derivative-free convex optimization#

A lower bound of order d²/log d on the number of exact function evaluations needed to minimize a convex Lipschitz function, closing a gap open since 1996 and showing a 1996 algorithm was essentially optimal.

In zeroth-order optimization an algorithm may only query a function's value, never its gradient. Protasov's 1996 algorithm needed about d² evaluations in d dimensions, but the best known lower bound was only about d, leaving open whether a much faster method existed. The new bound of Ω(d²/log(d+1)) matches the upper bound to polylogarithmic factors. Kerger reports that after a ten-page prompt built on his own earlier failed attempts, the model produced the complete proof in a single 2.5-hour session with no intervention; he then reviewed it and formally verified the core bound in Lean 4, which compiles against Mathlib with no `sorry` and no bespoke axioms.

WithPhillip Kerger

Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs#

An agent pairing language models with the Lean proof assistant resolved 9 of 353 open Erdős problems and 44 of 492 open OEIS conjectures, with every proof mechanically verified.

The system proposes proofs with a language model and checks every step in Lean, so a hallucinated argument cannot pass. Beyond the Erdős and OEIS totals it settled a 15-year-old question on log-concavity of pure O-sequences in codimension 3 and type 2, and proved an exact O(1/t) convergence rate for anchored gradient descent-ascent via a parameter choice not previously identified. Two of the Erdős problems had been open for 56 years. All formal proofs were released in a public repository.

WithPushmeet Kohli, Swarat Chaudhuri

Disproof of the Erdős unit-distance conjecture#

A reasoning model produced the core construction disproving a 1946 conjecture in discrete geometry, finding point configurations with more unit-distance pairs than the conjecture permitted.

The model found configurations showing the unit-distance count can grow at least as fast as n^1.014, exceeding the conjectured bound. Checked by external mathematicians including Fields Medalist Timothy Gowers, who called it 'the first example of a result produced autonomously by an AI that I find exciting in itself.'

Structure in Bruhat intervals of permutation groups#

AlphaEvolve identified unexpected special structure in Bruhat intervals for particular permutation groups.

Part of a continuing series of AlphaEvolve results in combinatorics. The system evolves candidate programs under a human-specified evaluation function, so the search is automated but the problem framing is human.

Erdős problem #728 resolved and formalized in Lean#

GPT-5.2 produced a proof of a previously open Erdős problem; Harmonic's Aristotle formalized it in Lean, making it the first Erdős problem regarded as fully resolved by AI with machine-checked proof.

The problem concerns the existence of infinitely many integers a, b, n satisfying divisibility and inequality conditions involving factorials. GPT-5.2 generated the argument, Aristotle formalized it in Lean, and a human-readable writeup was posted to arXiv. Modifications of the same argument also resolved problems #729 and #401.

Early science acceleration experiments with GPT-5#

A multi-domain study documenting cases where GPT-5 contributed to research progress across mathematics, physics, biology and materials science.

A collection of case studies rather than a single result. Useful as a source of individual entries; each contained claim needs separate grading before it belongs in the registry on its own.

AlphaEvolve across 67 problems: 20 improvements, 8 regressions#

A systematic study with Terence Tao of an evolutionary coding agent on 67 open problems in analysis, combinatorics and geometry, reporting where it beat the literature and where it did not.

Rather than a single headline result, this is the systematic version: 67 problems attempted, with outcomes recorded either way. Tao reports roughly 20 cases of a new result, most others matching known bounds, and 8 where the tool did worse than the literature. Genuine advances include new three-dimensional constructions for finite-field Nikodym sets, which then prompted a human-refined hybrid construction beating both algebraic and random baselines, and an improved upper bound for Sidon sets, from 1.96365 to about 1.9526. On the well-known conjectures of Sidorenko, Sendov and Crouzeix it found no counterexample, which Tao notes may simply reflect that they are true.

WithTerence Tao, Javier Gómez-Serrano, Bogdan Georgiev, Adam Zsolt Wagner

GPT-5 "solved 10 Erdős problems": it located existing solutions#

An OpenAI executive announced that GPT-5 had solved 10 previously open Erdős problems and made progress on 11 more; the problems were only 'open' in the sense that one database maintainer was unaware of the already-published solutions the model surfaced.

OpenAI VP Kevin Weil posted that 'GPT-5 found solutions to 10 (!) previously unsolved Erdős problems.' Thomas Bloom, who maintains erdosproblems.com, replied that listing a problem as open there only means he personally was unaware of a solution, and that GPT-5 had found existing papers containing the solutions rather than proving anything new. The post was deleted; Demis Hassabis called the episode 'embarrassing' and Yann LeCun mocked it.

Strong prime number theorem formalized in Lean by an autoformalization agent#

An agent completed a Lean formalization of the strong prime number theorem in about three weeks, finishing a project two expert mathematicians had left blocked after 18 months.

Tao and Kontorovich began a Lean formalization of the strong prime number theorem (the version with an explicit error term) in January 2024, and by July 2025 had announced intermediate progress blocked on core difficulties in complex analysis. Math, Inc. reports that Gauss produced over 25,000 lines of Lean and roughly 1,100 theorems and definitions in about three weeks, completing the project. The repository README states that most statements and proofs were produced by the agent, with humans supplying the high-level blueprint, reviewing key lemmas, and adapting prior work.

WithTerence Tao, Alex Kontorovich

Improved step-size bound in smooth convex optimization#

GPT-5 Pro extended a guaranteed-convexity window for gradient descent from η ≤ 1/L to η ≤ 1.5/L, but the optimal 1.75/L bound had already been published months earlier.

Bubeck posed an open problem from a convex optimization paper. After about 17 minutes of reasoning the model produced an improved bound using Bregman divergence inequalities and cocoercivity. Bubeck verified the proof as correct and described it as new mathematics.

WithSébastien Bubeck

4×4 complex matrix multiplication in 48 scalar multiplications#

AlphaEvolve found a scheme multiplying 4×4 complex matrices with 48 scalar multiplications, improving on Strassen's 49 from 1969.

Strassen's 1969 algorithm had stood at 49 multiplications for 56 years in this setting. AlphaEvolve was not purpose-built for matrix multiplication; it is a general evolutionary coding agent. The scheme is exactly checkable.

Improved lower bound for the 11-dimensional kissing number#

AlphaEvolve improved the best known configuration for the kissing number problem in 11 dimensions.

Part of a sweep across 50+ open problems in analysis, geometry, combinatorics and number theory. AlphaEvolve rediscovered state-of-the-art solutions in roughly 75% of cases and improved on the best known in about 20%. The kissing number problem asks how many non-overlapping unit spheres can touch a central one.

Improved bound for the Erdős minimum-overlap problem#

AlphaEvolve nudged the best known bound for Erdős's minimum-overlap constant, the first improvement since 2016, and sharpened several autocorrelation inequalities.

As part of a sweep across open problems in mathematical analysis, AlphaEvolve improved the upper bound on the Erdős minimum-overlap constant from about 0.380927 to about 0.380924, the first movement since 2016, and improved constants in autocorrelation inequalities. The gains are numerically small but exceed long-standing records, and the constructions are explicit and checkable.

Candidate treatment for dry age-related macular degeneration#

The Robin system automated hypothesis generation, experiment design and data analysis, identifying a novel candidate treatment for dry AMD.

Presented as an end-to-end automated discovery loop with humans executing the physical experiments.

AI co-scientist hypotheses on antimicrobial resistance and liver fibrosis#

A multi-agent system generated hypotheses that were subsequently validated experimentally in the lab.

The system proposed mechanisms in antimicrobial resistance and liver fibrosis that wet-lab work then supported. Notable as one of the earliest cases of an AI-generated hypothesis surviving experimental test rather than just sounding plausible.

Silver-medal standard at the 2024 International Mathematical Olympiad#

AlphaProof and AlphaGeometry 2 together solved four of the six 2024 IMO problems for 28 of 42 points (one short of the gold threshold), with the algebra and number-theory solutions produced and checked in the Lean proof assistant.

AlphaProof, a reinforcement-learning system that works inside Lean, solved two algebra problems and one number-theory problem (including P6, the competition's hardest, which few human contestants solved), while AlphaGeometry 2 solved the geometry problem in seconds. The two combinatorics problems went unsolved. The Lean-based solutions are machine-checked by construction; the full performance was graded by mathematicians Timothy Gowers and Joseph Myers under competition-style marking.

New lower bound constructions for the cap set problem#

FunSearch discovered larger cap sets than any previously known construction, the first time an LLM-based system produced a genuinely new discovery on an established open problem.

FunSearch pairs an LLM that proposes programs with an automated evaluator that rejects incorrect ones, sidestepping hallucination by construction. Applied to extremal combinatorics, it found new large cap sets in both finite-dimensional and asymptotic cases. Published in Nature. Historically the first entry in this registry's scope.

Improved heuristics for online bin packing#

FunSearch produced bin-packing heuristics outperforming standard baselines on benchmark distributions.

Discovered programs are human-readable, which allowed domain experts to inspect and deploy them. Practical rather than theoretical significance.

Large-scale prediction of new stable crystalline materials (GNoME)#

GNoME predicted about 2.2 million new inorganic crystal structures, roughly 380,000 of them flagged as thermodynamically stable, presented as an order-of-magnitude expansion of known stable materials.

Graph Networks for Materials Exploration (GNoME) is a graph neural network trained in an active-learning loop against density-functional-theory calculations to predict formation energies and filter candidates by stability. DeepMind released the predicted structures as a public dataset. Published in Nature.

Autonomous laboratory reports solid-state synthesis of new inorganic compounds#

Berkeley's A-Lab, an AI-driven autonomous laboratory, reported synthesising 41 novel inorganic compounds out of 58 targets over 17 days with minimal human intervention.

A-Lab coupled machine-learning synthesis-recipe prediction with robotic sample preparation, heating and X-ray characterisation, drawing targets from stability predictions including GNoME's. It reported making 41 of 58 targeted compounds autonomously. Published in Nature alongside GNoME.

Faster sorting routines discovered and merged into the LLVM C++ library#

AlphaDev found shorter branchless routines for sorting small fixed-length inputs; reverse-engineered to C++, they were merged into LLVM's libc++, the first change to those routines in over a decade.

AlphaDev treated the construction of a sorting routine as a single-player game played directly in CPU assembly, rewarding shorter and faster correct programs. For sort-3, sort-4 and sort-5 it removed instructions relative to the human-tuned library code, yielding large speedups on short sequences. The routines were reverse-engineered to C++ and accepted into the LLVM libc++ standard sort, which ships to millions of users. Published in Nature.

Faster matrix-multiplication algorithms found by reinforcement learning#

AlphaTensor discovered matrix-multiplication schemes using fewer scalar multiplications than any previously known, including a way to multiply 4×4 matrices over GF(2) in 47 multiplications versus the 49 of two-level Strassen.

AlphaTensor recast the search for matrix-multiplication algorithms as a single-player game of decomposing a 3-D tensor into rank-one terms, then trained an AlphaZero-style agent to play it. It matched or beat the best known rank for many matrix sizes, and over GF(2) found a 4×4 scheme using 47 multiplications, improving on the 49 obtained by applying Strassen's 1969 algorithm twice. Every decomposition it returns is an exact identity checkable by hand. Published in Nature.

Deep reinforcement learning controls tokamak fusion plasma#

A reinforcement-learning controller learned to shape and stabilise the magnetic confinement of real fusion plasma inside the TCV tokamak, holding configurations that are hard to sustain by hand.

Working with EPFL's Swiss Plasma Center, DeepMind trained a deep reinforcement-learning agent to command the magnetic control coils of the TCV tokamak. Learning in a simulator against specified target shapes, the controller then ran on the real machine, holding elongated, snowflake and other configurations, including a 'droplet' state with two separate plasmas at once. It is one of the first times a single learned controller replaced the hand-engineered cascade normally required.

Accurate protein structure prediction across the known proteome (AlphaFold2)#

AlphaFold2 predicted three-dimensional structures for nearly all catalogued proteins from amino-acid sequence at accuracy rivalling experiment, work that earned the 2024 Nobel Prize in Chemistry.

AlphaFold2 pairs an attention-based neural network with evolutionary sequence information to predict how a protein folds from its amino-acid sequence. At the 2020 CASP14 blind assessment it reached accuracy competitive with experimental methods, and DeepMind and EMBL-EBI then released predicted structures for over 200 million proteins, nearly the entire catalogued proteome. Demis Hassabis and John Jumper shared the 2024 Nobel Prize in Chemistry for the work, alongside David Baker for computational protein design.

WithJohn Jumper, Demis Hassabis