What has AI actually discovered in science and mathematics?

whataifound.org is a curated registry of scientific and mathematical results discovered by or with AI systems. Each entry records the claim, the AI model and lab involved, the human collaborators, and a grade for how it was verified and how much the AI actually did.

How does whataifound.org verify AI discoveries?

Every finding is graded on a verification scale from strongest to weakest: formally verified (machine-checked proof), independently checked, peer reviewed, author verified, claimed, disputed, already known, and refuted. When unsure, the lower grade wins. Nothing is ever deleted; entries are downgraded and annotated instead.

How much of an AI discovery was done by the AI versus humans?

whataifound.org grades an autonomy axis on the strictest defensible reading: autonomous, AI-led, collaborative, AI-assisted, search scaffold (e.g. FunSearch, AlphaEvolve), or retrieval. If a human posed the problem, suggested the approach, and checked the algebra, that is not counted as autonomous.

Has AI ever proved a new theorem?

Yes, and one case is machine-checked. In January 2026 GPT-5.2 produced a proof of the previously open Erdős problem #728, and Harmonic's Aristotle formalized it in Lean, making it the first Erdős problem regarded as fully resolved by AI with a machine-checked proof. Correctness there is essentially certain; significance is the contested part, as Terence Tao noted the problem was open but not considered deep. Separately, in May 2026 an OpenAI reasoning model produced the core construction disproving the 1946 Erdős unit-distance conjecture, checked independently by mathematicians including Timothy Gowers. whataifound.org grades the first as formally verified and autonomous, and the second as independently checked and AI-led.

Did AI really discover 2 million new materials?

That claim is disputed. Google DeepMind's GNoME predicted about 2.2 million new inorganic crystal structures in November 2023, roughly 380,000 flagged as thermodynamically stable. Reviewing the release, Cheetham and Seshadri found 'scant evidence for compounds that fulfil the trifecta of novelty, credibility and utility', noting many predictions are minor variations on known compounds rather than genuinely new materials. The objections remain unresolved. The companion A-Lab result, an autonomous laboratory reporting solid-state synthesis of new inorganic compounds, is also graded disputed after independent reanalysis challenged the claimed syntheses. whataifound.org grades both as disputed and keeps them on the record rather than deleting them.

Did GPT-5 solve 10 open Erdős problems?

No. In October 2025 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 existing solutions; the solutions were already in the published literature and GPT-5 located them. That is a genuinely useful literature-search result, but it was misdescribed as original discovery, and the claim was retracted. whataifound.org grades it as already known on the verification axis and retrieval on the autonomy axis, and keeps it as a cautionary entry.

Is AlphaFold an AI discovery?

Yes, and it is the strongest-verified entry of its kind. AlphaFold2 predicted three-dimensional structures for nearly all catalogued proteins from amino-acid sequence at accuracy rivalling experiment, solving a roughly fifty-year grand challenge and earning the 2024 Nobel Prize in Chemistry. whataifound.org grades it independently checked and AI-led. The important caveat is that AlphaFold predicts structures rather than determining them experimentally: its outputs are computational hypotheses that can be wrong for disordered regions, alternative folds, point mutations and many complexes.

How many AI discoveries are actually verified?

Of the 56 results currently on the whataifound.org register, 42 are well verified (formally verified, independently checked or peer reviewed) and 5 are negative or contested (already known, disputed or refuted). Only 21 are graded AI-led or autonomous; 23 came from human-built search scaffolds such as FunSearch and AlphaEvolve, where an LLM sits inside a harness a human designed. The register is deliberately small because each entry has to survive a novelty check, and refuted and already-known results stay on the record, marked as such.

whataifound.org: What AI Has Actually Discovered

Every link is labelled by what it is: the original work, the announcement, press coverage, independent commentary, or a challenge to the claim. Most of the distance between a result and a headline is in the last four. How we classify →

OpenAI

2026-08-01

Formally verified AI-led

Model: Astra
Field: mathematics
Posed: 1999 · open 27 yrs

Ten results in mathematics and theoretical computer science with Lean certificates #

An unreleased OpenAI model produced ten results including the first explicit non-sofic group and a disproof of Connes's rigidity conjecture, each published with a machine-checkable Lean 4 proof.

The ten cover high-dimensional sphere packing, binary and spherical codes, non-sofic groups, Connes's rigidity conjecture, arithmetic circuit complexity, quantum parallel repetition, the closest vector problem, Ehrhart's volume conjecture, multicolor Ramsey numbers and extremal number conjectures. Soficity was introduced by Gromov in 1999 and whether a non-sofic group exists had stood open since; Connes posed his rigidity conjecture in 1980, and the disproof constructs infinitely many non-isomorphic property (T) groups sharing a von Neumann algebra. Humans used the same model to prepare the manuscripts and then to formalize each argument in Lean 4.32.0. OpenAI put the token cost of finding all ten at roughly $2,000 at Sol API rates.

Original work: GitHub
Announced: OpenAI
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Each of the ten is a named open problem with a documented origin: soficity from Gromov 1999, Connes rigidity from 1980, and the sphere-packing exponent improvement is the first on the general bound since 1978. The Lean repository states which prior bound each result improves. Thomas Bloom, who maintains erdosproblems.com and publicly corrected OpenAI's 2025 Erdős retrieval episode, called these results big news, which is meaningful given that he is the person who caught the previous overclaim.

Caveats

The certificates are checkable and the claim that the theorems hold is as solid as Lean makes it. The claim about provenance is not checkable: Astra is unreleased, so no outside party can test whether the model produces these results, and the account of how they were found rests entirely on OpenAI. Grading verification as formal reflects the proofs, not the provenance; a reader who cares only about who found it should read this as claimed. Specialist review of the mathematical significance is still pending in several cases. Noam Brown noted there are no Millennium Prize problems here. Press summaries of the ten disagree with the repository's own list, some substituting specific Erdős problem numbers that do not appear in it; the list above follows the repository.

Original work

GitHubLean 4 certificates for all ten results↗

Announcement

OpenAITen advances in mathematics and theoretical computer science↗

Independent

2026-07-22

Claimed AI-led

Model: GPT-5.6 Pro
Field: computer-science
Posed: 1999 · open 27 yrs

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

combinatorial-optimization network-flow counterexample unsplittable-flow

Announced: X
Media: OfficeChai
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The Dinitz–Garg–Goemans unsplittable-flow result is from the late 1990s (D. Dinitz, N. Garg, M. Goemans, 'On the single-source unsplittable flow problem'); the cost-preserving strengthening was an open conjecture attributed to Goemans. No prior counterexample or resolution appears in the literature. The construction is a new concrete instance, not a retrieval of an existing example.

Caveats

Not peer-reviewed or machine-checked in a proof assistant. Verification rests on the author's own exhaustive-enumeration program over a finite instance, which anyone can rerun but which had no logged independent replication at announcement. The result was shared informally on X with a public GPT-5.6 Pro transcript. One third party (Hensen Juang) publicly generalized the instance into an infinite parametric family on the same seven nodes, which is consistent with the claim but is not a formal independent check. Autonomy graded ai-led: the model produced the construction; the human posed the problem and verified. Downgraded from 'author verified' when source classification showed no primary artifact is linked: the construction was published as a chat transcript rather than a paper or repository. Readers have checked the arithmetic and found it consistent, but there is nothing citable to point at, so the grade caps at 'claimed' until someone links a standalone write-up.

Announcement

XDmitry Rybin announcement (X)↗

Media coverage

OfficeChaiCoverage: officechai↗

Community discussion

XHensen Juang: infinite family generalizing the counterexample (X)↗

Independent

2026-07-20

Author verified AI-led

Model: GPT-5.6 Sol Pro + Claude Fable 5
Field: mathematics
Posed: 2017 · open 9 yrs

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

algebra polynomial-maps counterexample jacobian-conjecture

Original work: arXiv arXiv
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The Gaussian moments conjecture is due to Derksen, van den Essen and Zhao (Israel J. Math., 2017), building on their earlier moment-vanishing and integral conjectures. No prior counterexample appears in the literature; the conjecture's interest was precisely that it implied the Jacobian conjecture, which was disproved on 2026-07-19. The two-variable case GMC(2) is explicitly left open by this paper.

Caveats

arXiv preprint, not peer-reviewed, single author. The constructions are explicit polynomials and checkable by computer algebra, which lowers the cost of verification, but no independent check is on the public record yet. The result is a corollary of the Jacobian collapse rather than an independent line of attack: the prompt that produced it began by telling the model that the Jacobian conjecture had fallen.

Original work

arXivSmall Counterexamples to the Gaussian Moments Conjecture↗arXivDerksen, van den Essen, Zhao: The Gaussian Moments Conjecture and the Jacobian Conjecture↗

Harmonic

2026-07-20

Formally verified Autonomous

Model: Aristotle
Field: mathematics
Posed: 1969 · open 57 yrs

Eight problems from the Kourovka Notebook solved and formalized in Lean #

A formal reasoning agent developed the proof strategies for eight open problems in group theory without human guidance on which mathematical steps to take, and machine-checked every one in Lean 4.

The Kourovka Notebook has collected open problems in group theory since 1965, with a new issue every two to four years. Aristotle solved eight of them: 3.46 (a group with exactly two maximal locally soluble normal subgroups), 18.50, 19.25, 20.125 (a surjective non-injective Rota-Baxter operator on a non-abelian group), 21.8, 21.24, 21.147 and 21.150. The oldest first appeared in the third issue in 1969. Solutions take the form of proofs, counterexamples and constructions, each formalized in Lean 4 and published in a companion repository. The authors then informalized the Lean proofs into conventional prose and submitted both to the Notebook editors and the original problem proposers, who accepted them before publication.

WithWouter van Doorn, Elias Judin, Pietro Monticone, Daniel Morrison

group-theory lean formalization kourovka-notebook autonomous-discovery

Original work: arXiv GitHub
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The Kourovka Notebook is itself the authoritative open-problems register for group theory, and each of the eight is recorded there as open with a named proposer, so novelty is established by the source of record rather than by a literature search. The authors submitted solutions to the Notebook editors and the problem proposers for acceptance before publishing, and the initial submissions remain in the Notebook's own preprint repository. Problem 3.46 traces to Plotkin's survey question on products of locally soluble normal subgroups, which Baumslag, Kovács and Neumann had partly addressed in the negative.

Caveats

Not peer reviewed as a journal article, though the individual solutions were accepted by the Kourovka Notebook editors and the problem proposers, which is the relevant gatekeeping for this venue. The autonomy grade rests on the authors' own disclosure: they state Aristotle developed the proof strategies without human guidance about which steps to take, while they monitored its work, intervened when clarifications were needed, and built a library of relevant concepts with it. That library work and the final canonisation for Mathlib upstreaming were done partly by hand. The Lean certificates are the load-bearing evidence and anyone can rerun them; the claim about how the arguments were found rests on the authors' account.

Original work

arXivOn Some Problems from the Kourovka Notebook↗GitHubLean 4 formalizations of all eight solutions↗

Anthropic

2026-07-19

Formally verified Collaborative

Model: Claude Fable 5
Field: mathematics
Posed: 1939 · open 87 yrs

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

algebraic-geometry counterexample polynomial-maps

Original work: jacobianfun.org
Commentary: Alexis Gallagher Hacker News
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The Jacobian conjecture (Keller, 1939) has been a celebrated open problem for 87 years, with many published false proofs in both directions. No prior counterexample in any dimension over characteristic 0 exists in the literature. Ott-Heinrich Keller's original formulation is the one addressed.

Caveats

Not yet peer-reviewed. The formula is public and checkable in seconds by computer algebra, which makes conventional peer review less load-bearing than usual, but the official record lists the conjecture as open until the literature catches up. The division of labor between Alpöge and the model has not been fully documented; autonomy graded conservatively pending a transcript.

Independent checks

whataifound.org (symbolic recomputation, SymPy): confirmed, det J = −2 identically; all three points map to (−¼,0,0)

Multiple mathematicians via public computer-algebra checks: confirmed · link ↗

Original work

jacobianfun.orgThe Jacobian counterexample, explained↗

Independent commentary

Alexis GallagherJacobian Conjecture Disproved!↗Hacker NewsHacker News discussion↗

Independent

2026-07-14

Formally verified AI-led

Model: GPT-5.6 Sol Pro
Field: mathematics
Posed: 1996 · open 30 yrs

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

optimization complexity-theory lower-bounds lean

Original work: arXiv GitHub
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The gap between Protasov's O(d²) upper bound (1996) and the O(d) lower bound is documented in the derivative-free optimization literature and had stood for three decades. No prior matching lower bound appears in the literature. The paper is explicit that the AI produced the argument.

Caveats

arXiv preprint, not peer-reviewed. The author states plainly that 'it is accurate to say that the AI model used solved the problem, not the author of this paper', which is the basis for the ai-led grade; the human wrote the prompt, reviewed the proof, and did the Lean formalization. Graded `formal` on the strength of the machine-checked Lean artifact for the core bound, not on the preprint as a whole.

Independent checks

Lean 4 / Mathlib compiler (author-run, artifact public): core Ω̃(d²) lower bound compiles with no sorry and no bespoke axioms · link ↗

Original work

arXivClosing the Oracle-Complexity Gap in Derivative-Free Convex Optimization↗GitHubLean verification, prompt and chat logs↗

Independent

2026-07-11

Formally verified Collaborative

Model: OpenAI Sol (construction); Claude Fable (Lean formalisation)
Field: mathematics

Counterexample to Grothendieck's question on finite flat group schemes #

A finite locally free group scheme of order four whose fourth power map is not trivial, answering a question Grothendieck raised in the 1960s; one model produced the construction and another formalised it in Lean.

Grothendieck asked whether every finite locally free group scheme of order n is killed by n. Deligne proved it for commutative group schemes; the non-commutative case stayed open. The counterexample is a Hopf algebra of rank four over the ring Z[a,b]/(a³, b³, a²b+2), with coordinate algebra R[U,V]/(U² − abU + b²V, V² − a²V), whose fourth convolution power is not the convolution unit. Kevin Buzzard, told of a 12-page informal write-up, replied that he does not read AI-generated informal mathematics and asked for a Lean proof instead; four hours later a 1,076-line Lean formalisation existed, and it compiles on a laptop in under five minutes. It was submitted to mathlib as pull request #41748.

WithAkhil Mathew, Kevin Buzzard

algebraic-geometry group-schemes counterexample lean formalization

Original work: GitHub
Announced: Kevin Buzzard
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Per Buzzard's account, the question had been settled in special cases by Grothendieck, Deligne and René Schoof, with further partial results published by Emiliano Torti in 2025; no counterexample appeared in the literature. The object here is an explicit new construction rather than a rediscovered example, and the Lean file states and refutes the general claim directly.

Caveats

The mathlib pull request was open, not merged, when this entry was written, and was filed by a pseudonymous account whose module docstring credits "Codex (OpenAI) and Claude (Anthropic), under the direction of the author" rather than naming Sol or Fable; the model attribution here follows Buzzard's blog post. The `formal` grade rests on the Lean proof compiling, which Buzzard reports doing himself; the 12-page informal argument has not been peer reviewed. Autonomy graded collaborative: a human posed the question, directed the work and filed the PR, and the record of who did which step is a blog post rather than a transcript.

Independent checks

Kevin Buzzard (compiled the Lean formalisation): confirmed; 1,076-line Lean proof compiles in under five minutes · link ↗

Original work

GitHubmathlib4 PR #41748: a finite free group scheme of order four not killed by four↗

Announcement

Kevin BuzzardHuman mathematicians are being outcounterexampled↗

Vesuvius Challenge

2026-06-25

Author verified AI-assisted

Model: Community-developed ink-detection neural networks
Field: archaeology

First Herculaneum scroll read end to end without unrolling it #

PHerc. 1667 was virtually unwrapped and read in full from X-ray scans using learned ink detection: about 1.4 metres of papyrus across roughly 22 columns of Greek, identified as Philodemus, On Gods, Book 8.

The Herculaneum scrolls were carbonised by the AD 79 eruption of Vesuvius and disintegrate if physically unrolled. The pipeline scans a scroll by X-ray tomography, traces the rolled sheet as a three-dimensional surface, flattens it, and runs a network that detects near-invisible carbon ink from sub-millimetre surface texture. Luke Farritor's model recovered the first word, πορφύρας ("purple"), in October 2023, and the 2023 Grand Prize for four passages of 140 characters was claimed in February 2024. In June 2026, PHerc. 1667 became the first scroll recovered continuously from beginning to end, and a title read in a related scroll established that Philodemus' On Gods ran to at least eight books.

WithBrent Seales, Luke Farritor, Youssef Nader, Julian Schilliger

papyrology virtual-unwrapping ink-detection ancient-texts

Original work: arXiv
Announced: Vesuvius Challenge Vesuvius Challenge
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Virtual unwrapping itself is older (Seales read the En-Gedi scroll in 2015), but that worked because its ink contained metal and showed up in X-ray. Herculaneum ink is carbon-based and nearly invisible to tomography, which is why the ink signal had to be learned from texture instead of density. No Herculaneum scroll had been read by any method before this programme.

Caveats

Readings are probabilistic reconstructions from a learned ink signal, not photographs of text: characters come with varying confidence and papyrologists supply conventional editorial restoration on top. The project's papyrology team reviews prize submissions, but that team is part of the challenge rather than an outside body, and no peer-reviewed critical edition of PHerc. 1667 had appeared when this entry was written, hence author-verified rather than independent. The attribution to Philodemus rests on a title read in a different scroll.

Original work

arXivComplete virtual unwrapping and reading of a rolled Herculaneum papyrus↗

Announcement

Vesuvius ChallengeAn entire Herculaneum scroll has been read for the first time↗Vesuvius ChallengeVesuvius Challenge↗

Aalto University / Rice University

2026-06-17

Peer reviewed Search scaffold

Model: Unknown
Field: materials

Two kagome superconductors predicted by machine learning and confirmed in the lab #

A screening pipeline that narrowed over 1.3 million candidate structures picked out YRu3B2 and LuRu3B2, which were then synthesized and measured to superconduct at 0.81 K and 0.95 K.

The SuperC consortium used machine-learning pre-screening to cut a very large chemical space down to a tractable candidate list, then ran first-principles calculations on what survived, arriving at 741 dynamically and thermodynamically stable compounds with DFT-predicted Tc above 5 K. Morosan's group at Rice synthesized two of them and confirmed bulk superconductivity by magnetization and specific heat measurement. Both compounds carry a kagome lattice, in which electrons form flat bands.

WithRose Albu Mustaf, Päivi Törmä, Emilia Morosan, B. Andrei Bernevig, Miguel A. L. Marques

superconductivity kagome high-throughput-screening dft experimental-confirmation

Original work: arXiv
Media: ScienceDaily
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Machine-learning screening of superconductor candidates is an established and crowded field, and the JHU APL work on novel superconductors predates this. What is claimed as new is the end-to-end path: candidates identified from scratch by a machine-learning-guided pipeline, then synthesized and experimentally confirmed, rather than screening validated only against already-known superconductors. YRu3B2 and LuRu3B2 were not previously reported as superconductors. Whether this is the first such end-to-end confirmation is the consortium's framing and is not independently adjudicated here.

Caveats

The gap between prediction and measurement is the story the coverage mostly buries: the screen selected for DFT-predicted Tc above 5 K, and the two compounds actually measured at 0.81 K and 0.95 K, roughly a factor of five to six low. These are sub-1-kelvin superconductors, nowhere near room temperature, and the consortium's stated goal of a room-temperature superconductor by 2033 is a research programme, not a result. Two confirmed compounds out of 741 stable candidates is also not a hit rate the paper establishes as generalizable. The specific machine-learning method is not named in the coverage consulted, so model is recorded as Unknown.

Original work

arXivMachine Learning-Guided Discovery of Kagome Superconductors YRu3B2 and LuRu3B2↗

Media coverage

ScienceDailyAI just supercharged the race to find room temperature superconductors↗

Google DeepMind

2026-05-21

Formally verified Search scaffold

Model: AlphaProof Nexus (LLM + Lean)
Field: mathematics

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

lean automated-theorem-proving erdos-problems combinatorics

Original work: arXiv GitHub GitHub
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The Erdős problems were listed as open in the erdosproblems.com database and the OEIS conjectures as unproven at the time of the run; the paper documents which. In the course of the work the authors found misformalizations in the stated problems #125 and #741(i), which had to be corrected before resolution, a reminder that 'open' status in a database is itself fallible. Terence Tao's community wiki independently tracks AI contributions to Erdős problems and records these.

Caveats

The headline is a hit rate, not a sweep: 9 of 353 and 44 of 492. The authors state successes concentrate in combinatorics, convex optimization and number theory where Lean's library is mature, that the agent inherits its LLM's biases and shows high search variance, and that it cannot solve problems requiring substantial new theory. Formal verification guarantees the proofs are correct; it says nothing about whether the problems were deep. Autonomy is graded search-scaffold rather than autonomous: humans built the agent, chose the problem sets, and supplied the formalization targets.

Independent checks

Lean compiler via the paper's SafeVerify step: all proofs compile with no sorry and no disallowed axioms (sorryAx) · link ↗

Terence Tao's AI-contributions wiki: tracked among AI contributions to Erdős problems · link ↗

Original work

arXivAdvancing Mathematics Research with AI-Driven Formal Proof Search↗GitHubAll Lean proofs (DeepMind repository)↗GitHubTao's AI-contributions-to-Erdős-problems wiki↗

OpenAI

2026-05-20

Independently checked AI-led

Model: GPT-5 series reasoning model
Field: mathematics
Posed: 1946 · open 80 yrs

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 produced a construction beating the conjectured bound, with an inexplicit exponent greater than 1. Nine mathematicians - Alon, Bloom, Gowers, Litt, Sawin, Shankar, Tsimerman, Wang and Wood - published a human-verified version of the argument; Sawin separately made the exponent explicit at n^1.014. Gowers called it 'the first example of a result produced autonomously by an AI that I find exciting in itself.'

discrete-geometry combinatorics erdos

Original work: arXiv arXiv
Media: Quanta TechCrunch Tech Jacks
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The unit-distance problem dates to Erdős (1946). Prior bounds were well documented; the construction is new.

Caveats

Human mathematicians shaped the problem framing and verified the construction. The explicit n^1.014 exponent is Sawin's refinement, not the model's output: the model's own bound was inexplicit. The strength of the endorsement from Gowers is notable but is a judgment, not a formal check.

Original work

arXivRemarks on the disproof of the unit distance conjecture (human-verified writeup)↗arXivSawin: An explicit lower bound for the unit distance problem↗

Media coverage

QuantaThe AI Revolution in Math Has Arrived↗TechCrunchOpenAI claims it solved an 80-year-old math problem, for real this time↗Tech JacksAI math reasoning milestones↗

University of Cambridge / DIOSynVax

2026-05-18

Peer reviewed AI-assisted

Model: Unknown
Field: medicine

Phase 1 trial of a computationally designed pan-sarbecovirus vaccine #

A vaccine whose antigen was designed entirely in silico from sarbecovirus sequence data was safe in 39 healthy volunteers and raised immune responses against SARS-CoV-2, SARS, and bat viruses that have never infected humans.

Rather than target one strain, the team analysed sarbecovirus genetic data to compute a single synthetic antigen capturing structural features shared across the subgenus, on the theory that a vaccine aimed at what the family has in common survives the evolution of any one member. The candidate, pEVAC-PS, is a DNA vaccine delivered needle-free by micro fluid jet. The phase 1 dose-escalation trial ran in 39 healthy volunteers aged 18 to 50, sponsored by University Hospital Southampton NHS Foundation Trust, and reported no significant side effects.

WithAlasdair P. S. Munro, Jonathan L. Heeney, Saul N. Faust

vaccine-design clinical-trial coronavirus antigen-design phase-1

Original work: Journal of Infection
Announced: Cambridge
Media: ScienceDaily
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Computationally designed and consensus or mosaic antigens have a long history in HIV and influenza vaccine work, and broad sarbecovirus vaccine candidates were pursued by several groups after 2020. What is new here is a first-in-human safety and immunogenicity readout for an antigen with no natural sequence, generated computationally rather than selected from circulating strains. Searched PubMed for prior phase 1 results on pan-sarbecovirus immunogens; earlier candidates in this class were preclinical at the time of publication.

Caveats

Phase 1: safety, tolerability and immunogenicity only. No efficacy claim, and immune response is not protection. n=39, healthy adults 18 to 50, so nothing follows about older or immunocompromised populations. Approval is years away and a phase 2 is planned. The autonomy grade is deliberately conservative because the public record is thin on what the computational method actually was: the reporting says artificial intelligence and machine learning without naming a model, architecture or developer, so model is recorded as Unknown rather than inferred. The bat-virus immunogenicity result is a laboratory assay against viruses that have not infected humans, not evidence of protection against a future outbreak.

Original work

Journal of InfectionA phase I, needle free, dose escalation clinical trial of pEVAC-PS, a candidate pan-Sarbecovirus vaccine↗

Announcement

CambridgeUniversity of Cambridge: New universal vaccine technology could protect us from future virus outbreaks↗

Media coverage

ScienceDailyAI-designed universal coronavirus vaccine passes first human trial↗

Google DeepMind

2026-01-15

Independently checked Search scaffold

Model: AlphaEvolve (Gemini-based)
Field: mathematics

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.

combinatorics alphaevolve

Original work: arXiv
Media: Quanta
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Documented as a new observation in the Quanta coverage; the specific structure was not previously catalogued.

Caveats

The paper is an arXiv preprint, not yet peer reviewed, so this entry was downgraded from 'peer reviewed' once the artifact was located. The five authors are academic mathematicians unaffiliated with the announcing lab, and they turned AlphaEvolve's suggested permutations into proved theorems, which is what the 'independently checked' grade rests on.

Original work

arXivEllenberg, Libedinsky, Plaza, Simental, Williamson: Bruhat intervals that are large hypercubes↗

Media coverage

QuantaThe AI Revolution in Math Has Arrived↗

OpenAI / Harmonic

2026-01-13

Formally verified Autonomous

Model: GPT-5.2 Pro + Aristotle
Field: mathematics

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.

number-theory erdos lean formalization

Original work: arXiv GitHub
Media: The Decoder
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Recorded as open in the Erdős problems database prior to resolution. Terence Tao's AI-contributions wiki tracked the resolution and did not find the result in existing literature.

Caveats

Tao cautioned that the win 'says more about speed than difficulty': the problem was open but not considered deep. Lean formalization makes correctness essentially certain; significance is the contested part, not validity.

Independent checks

Lean kernel (machine-checked): verified · link ↗

Terence Tao: accepted · link ↗

Original work

arXivarXiv 2601.07421: Resolution of Erdős Problem #728↗GitHubTao: AI contributions to Erdős problems↗

Media coverage

The DecoderTao on GPT-5.2 Pro↗

OpenAI

2025-11-20

Peer reviewed AI-assisted

Model: GPT-5
Field: computer-science

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.

meta multi-domain

Original work: arXiv
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Not applicable. This is a meta-report, not a single claim.

Caveats

Lab-authored evaluation of its own model. Individual case studies vary widely in strength and several have not been independently checked.

Original work

arXivarXiv 2511.16072↗

Google DeepMind

2025-11-03

Independently checked Search scaffold

Model: AlphaEvolve (Gemini-based)
Field: mathematics

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

combinatorics geometry analysis evolutionary-search

Original work: arXiv
Announced: Terence Tao
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Prior bounds are cited per problem in the 81-page paper, with data and prompts released publicly. Tao flags the central novelty risk himself: for well-known problems the tool often proposed the optimal construction immediately, suggesting recall from training data rather than search, and one supposedly new four-dimensional Kakeya construction turned out to essentially match a prior Bukh–Chao paper. Entries in this registry drawn from the earlier AlphaEvolve release (kissing number, minimum overlap, matrix multiplication) are tracked separately.

Caveats

Tao's own framing is that the contribution is scale and adaptability, not a fundamental breakthrough, and he describes the LLM as supplying 'educated randomness' inside an evolutionary loop rather than doing symbolic reasoning. Substantial human expertise was required to design non-exploitable verifiers: the system reliably finds loopholes, such as placing points at nearly identical locations to satisfy a distance tolerance. Included here because the negative and null results are reported alongside the wins, which is rare and is what makes it citable.

Independent checks

Terence Tao (co-author, published assessment): reports ~20 new results, 8 worse than literature; cautions on training-data contamination · link ↗

Original work

arXivMathematical exploration and discovery at scale↗

Announcement

Terence TaoTerence Tao's write-up↗

OpenAI

2025-10-19

Already known Retrieval

Model: GPT-5
Field: mathematics

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.

number-theory erdos already-known cautionary retrieval

Challenge: TechCrunch The Decoder

Novelty check, caveats & sources

Novelty check

By definition, that is the whole point of the episode. The solutions existed in the published literature; GPT-5's contribution was locating them, a genuinely useful literature-search result that was misdescribed as original problem-solving.

Caveats

Retained as a cautionary entry and a direct companion to the GPT-5 convex-optimization case. The underlying literature search was real and valuable; only the 'solved previously unsolved problems' framing was false. This is distinct from the later, genuine GPT-5.2 + Aristotle resolution of Erdős #728.

Independent checks

Thomas Bloom (erdosproblems.com maintainer): the problems were already solved in the literature; no new proofs · link ↗

Challenge

TechCrunchOpenAI's 'embarrassing' math↗The DecoderA GPT-5 math breakthrough that never happened↗

Community discussion

Hacker NewsOpenAI researcher announced a GPT-5 math breakthrough that never happened↗

UT Austin / CWI Amsterdam

2025-09-25

Author verified AI-assisted

Model: GPT-5 Thinking
Field: computer-science

Limits to black-box amplification in QMA, with the key step written by GPT-5 #

A quantum complexity paper proving black-box error amplification for QMA cannot push completeness closer to certainty than doubly exponentially, in which the pivotal technical step was produced by GPT-5 in about half an hour.

The authors were stuck on how the largest eigenvalue of a matrix behaved as a parameter varied. GPT-5 proposed reformulating the quantity so that a complex approximation-theory bound applied, and that reformulation became the technical core of the oracle separation. Aaronson wrote that the step would have cost him or a graduate student a couple of weeks and that it was the first substantive AI contribution to a paper of his. The result makes his 2008 oracle separation quantitative and shows recent amplification results are optimal for black-box procedures.

WithScott Aaronson, Freek Witteveen

quantum-complexity proof-assistance oracle-separation

Original work: arXiv
Announced: Scott Aaronson
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The theorem extends Aaronson's 2008 QMA oracle separation and a 2025 result of Jeffery and Witteveen; no prior bound of this form on black-box amplification appears in the literature. The AI contribution is documented in the paper's acknowledgements and on Aaronson's own blog, not inferred from press coverage. That matters, because most "AI proved a theorem" stories are not.

Caveats

An arXiv preprint. The contribution is one lemma inside a human-conceived and human-written paper; Aaronson is explicit that the model did not pose the problem or design the argument and that he could have done the step himself given time. Autonomy is ai-assisted, which stays the right grade even though the step was pivotal.

Original work

arXivLimits to black-box amplification in QMA↗

Announcement

Scott AaronsonThe QMA Singularity↗

Google DeepMind (with Brown, NYU and Stanford)

2025-09-17

Author verified Search scaffold

Model: Physics-informed neural networks with Gauss–Newton optimisation
Field: mathematics

New families of unstable singularities in fluid equations #

Physics-informed neural networks found previously unknown unstable self-similar blow-up solutions for three fluid equations, computed to near machine precision, and revealed an unexpected near-linear relation between a solution's instability order and its blow-up rate.

A physics-informed neural network minimises the residual of the differential equation itself rather than fitting data, which lets it hunt for self-similar blow-up profiles that ordinary simulation cannot hold onto because they are repelling. The team reports a stable and three unstable singularities for the incompressible porous media equation, a stable and three unstable solutions plus a candidate fourth for 2D Boussinesq, and an unstable singularity for 3D Euler with boundary. Residuals were driven near machine precision, the accuracy level a later computer-assisted proof would need. Across equations the blow-up rate depends almost linearly on the order of instability, a pattern nobody had predicted.

WithJavier Gómez-Serrano, Tristan Buckmaster, Ching-Yao Lai, Yongji Wang

pde fluid-dynamics singularity physics-informed-neural-networks

Original work: arXiv
Announced: DeepMind
Media: Physics World
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Stable self-similar blow-up for these equations was already known, including Chen and Hou's computer-assisted proof for 3D Euler with boundary. Unstable singularities had been found only in isolated cases because they are numerically repelling; no systematic families existed in the literature. This is the first paper to produce several unstable families across three different equations by one method.

Caveats

An arXiv preprint, not peer reviewed at the time of this entry. These are high-precision numerical solutions, not theorems: converting them into proofs requires a computer-assisted verification step the paper leaves to future work. No singularity for 3D Navier–Stokes, the Millennium Prize problem, is claimed, and the equations studied are not that one. Autonomy is search-scaffold: the equations, the self-similar ansatz and the loss function are human-designed and the network is the solver.

Original work

arXivDiscovery of Unstable Singularities↗

Announcement

DeepMindDiscovering new solutions to century-old problems in fluid dynamics↗

Media coverage

Physics WorldNeural networks discover unstable singularities in fluid systems↗

Arc Institute / Stanford University

2025-09-17

Peer reviewed AI-led

Model: Evo 1 and Evo 2
Field: biology

AI-generated bacteriophage genomes that replicate and kill bacteria #

Genome language models wrote complete ΦX174-like bacteriophage genomes from scratch; of 285 designs that could be built, 16 produced viable infectious phages, several with faster lysis than the natural virus.

The team fine-tuned Evo 1 and Evo 2 on a cleaned set of nearly 15,000 Microviridae genomes, generated 302 candidate genomes with ΦX174-like architecture, chemically synthesised the 285 that could be assembled, and tested them for plaque formation in E. coli. Sixteen were viable, with substantial sequence divergence from the template. Several generated phages outcompeted wild-type ΦX174 in growth and lysis kinetics, and a cocktail of them cleared three ΦX174-resistant E. coli strains. The authors frame it as the first generative design of a complete functional genome.

WithSamuel King, Brian Hie

genome-design bacteriophage generative-biology biosecurity

Original work: Science bioRxiv
Announced: Arc Institute
Media: Asimov Press
Commentary: Science
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Synthetic phage genomes assembled from natural sequence date to Venter's 2003 ΦX174 reconstruction, and generative design of individual proteins was well established. Generating an entire genome that yields a working organism had not been demonstrated. The claim is bounded to bacteriophages, which infect bacteria only.

Caveats

Peer review does not replicate: no independent group has rebuilt these genomes, and the 16 viable designs remain the authors' own result. The designs are variants within one small, exceptionally well-characterised template (ΦX174, 5,386 bp), not free-form genomes, and 269 of the 285 that were built did not work. On biosafety, the authors excluded eukaryotic and human-infecting viruses from training and confine the work to phages; the result has nonetheless become a reference point in biosecurity debate, which is context this entry records rather than adjudicates. Science published a biosecurity perspective alongside the paper arguing for legally required screening of synthetic DNA orders. Note that some press coverage of the Science paper misattributes the work to OpenAI; the collaboration is Arc Institute and Stanford.

Original work

ScienceGenerative design of bacteriophages with genome language models↗bioRxivGenerative design of novel bacteriophages with genome language models↗

Announcement

Arc InstituteHow we built the first AI-generated genomes↗

Media coverage

Asimov PressAI-designed phages↗

Independent commentary

ScienceInglesby and Hanke: Guarding against the misuse of AI-designed viruses↗

Math, Inc.

2025-09-11

Author verified AI-assisted

Model: Gauss (autoformalization agent)
Field: mathematics

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

lean formalization number-theory prime-number-theorem

Original work: GitHub
Announced: Math Inc.
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The prime number theorem is not new mathematics; the contribution is formalization. What was open was whether this particular formalization could be completed, and the surrounding claim is about speed. Recorded because formalization at this scale is a distinct kind of contribution and because the AI finished work humans had started and stalled on, rather than producing a new theorem. Prior art is the PrimeNumberTheoremAnd project itself, which this build reuses and which the README credits.

Caveats

This is a formalization result, not a mathematical discovery: no new theorem was proved. The comparison to '18+ months' is not like-for-like: Tao and Kontorovich worked intermittently, and the repository explicitly reuses definitions and some proofs from their earlier PrimeNumberTheoremAnd project. Math, Inc.'s announcement states the agent 'relies on natural language scaffolding supplied by human mathematicians, and requires high-level expert guidance'; the proportion of human effort is not quantified, and neither Tao nor Kontorovich is quoted in it. Graded author-verified rather than formal: the artifact is public and Lean-checkable, but the README does not itself assert a sorry-free build and no independent audit of that is on the public record. Vendor-announced, so the framing carries the usual caution.

Independent checks

Public Lean artifact (not independently audited): repository public and machine-checkable; README reports the development finished · link ↗

Original work

GitHubstrongpnt Lean repository↗

Announcement

Math Inc.Math, Inc.: Introducing Gauss↗

OpenAI

2025-08-01

Already known AI-assisted

Model: GPT-5 Pro
Field: mathematics

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

optimization already-known cautionary

Challenge: HackMD AllThings.how

Novelty check, caveats & sources

Novelty check

Version 2 of the source paper, published 2 April 2025, had already established the optimal 1.75/L bound, strictly stronger than the model's 1.5/L. The model was working from an earlier version and its result was superseded before it was produced.

Caveats

The proof itself is valid; the novelty claim is not. Analysts noted the argument largely recombined known techniques in different notation. Retained as a cautionary entry: this is the single most common failure mode in this space, and the reason every entry carries a novelty check.

Challenge

HackMDAnalysis of the claim↗AllThings.howWhat does GPT-5's 'new math' claim actually mean?↗

Community discussion

Hacker Newsclaim that GPT-5-pro can prove new interesting mathematics↗

Harmonic

2025-07-28

Formally verified AI-led

Model: Aristotle
Field: mathematics

Machine-checked Lean proofs for five of six 2025 IMO problems #

Harmonic's Aristotle produced formally verified Lean 4 proofs for five of the six 2025 IMO problems, so the gold-medal-standard score rests on a compiler rather than on human graders.

Aristotle drafts an informal proof, breaks it into intermediate lemmas, formalises each in Lean 4, and iterates against the compiler's feedback, which lets it use the large natural-language corpus of mathematics while still emitting machine-checked output. Harmonic published the Lean artifacts for the 2025 problems in a public repository. The announcement came a week after the natural-language gold results from Google DeepMind and OpenAI.

olympiad lean formalization benchmark

Original work: arXiv GitHub
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Formal IMO results are not new (AlphaProof solved three 2024 problems in Lean), but a gold-medal-level score with a formal proof for every claimed solution had not been reported. The problems have published official solutions, so this is a capability milestone rather than new mathematics.

Caveats

Problems had to be stated formally in Lean before the system could attempt them, the same human step that capped AlphaProof's autonomy grade. Answer-construction problems require the answer to appear in the formal statement, a known weakness of formal olympiad evaluation. No IMO-certified grading and no independently enforced contest time limit. The `formal` grade covers the proofs Aristotle produced, not the claim that this equals a human gold medal.

Original work

arXivAristotle: IMO-level Automated Theorem Proving↗GitHubharmonic-ai/IMO2025: Lean proofs and verification artifacts↗

Google DeepMind

2025-07-21

Independently checked AI-led

Model: Gemini Deep Think (advanced version)
Field: mathematics

Gold-medal standard at the 2025 International Mathematical Olympiad #

An advanced version of Gemini Deep Think read the official problem statements and wrote natural-language proofs for five of the six 2025 IMO problems inside the contest time limits, scoring 35 of 42, graded and certified by the official IMO coordinators.

The model worked end to end in natural language within the two 4.5-hour sessions, with no human translating problems into a formal language, and solved problems one through five. Google DeepMind was in the first cohort whose results were officially graded and certified by IMO coordinators against the rubric used for student scripts; 35 points is the gold-medal threshold. OpenAI announced the same 35/42 score two days earlier with an experimental reasoning model, graded internally by three former IMO medallists rather than by the IMO.

olympiad benchmark natural-language-proof

Original work: DeepMind
Announced: DeepMind
Commentary: Simon Willison
Challenge: none linked

Novelty check, caveats & sources

Novelty check

IMO problems have published official solutions, so this is a capability milestone rather than a new mathematical result, and the registry records it as one. The prior best was AlphaProof and AlphaGeometry 2's 28/42 in 2024, which required humans to hand-translate each problem into Lean first; removing that step is the substantive change.

Caveats

Benchmark performance on problems with known answers, not a discovery. Google's own account describes training on a curated corpus of high-quality solutions and providing general guidance on how to approach IMO problems, which is human mathematical input beyond posing the problem, hence ai-led rather than autonomous. Problem six went unsolved. The parallel OpenAI claim is self-graded and not IMO-certified, and drew criticism for being published before the closing ceremony, which organisers had asked AI developers to wait for.

Independent checks

Official IMO coordinators (certified grading): 35/42, gold-medal standard · link ↗

Original work

DeepMindGemini Deep Think: official IMO 2025 solutions (PDF)↗

Announcement

DeepMindGemini with Deep Think officially achieves gold-medal standard at the IMO↗

Independent commentary

Simon WillisonOpenAI's gold medal performance on the IMO↗

Insilico Medicine

2025-06-03

Peer reviewed Search scaffold

Model: PandaOmics (target) + Chemistry42 (molecule)
Field: medicine

Phase 2a results for a drug whose target and molecule both came from AI #

Rentosertib, a TNIK inhibitor whose target was picked by one AI system and whose molecule was generated by another, improved forced vital capacity by 98.4 mL at the top dose against a 20.3 mL decline on placebo in a 71-patient randomised trial.

TNIK was prioritised as a fibrosis target by PandaOmics from omics and literature data; the inhibitor was generated and optimised by Chemistry42. GENESIS-IPF was a 12-week double-blind placebo-controlled Phase 2a across 22 sites in China, randomising 71 idiopathic pulmonary fibrosis patients across placebo and three dose arms. The 60 mg once-daily arm showed the largest lung-function improvement, and the drug was generally well tolerated. Published in Nature Medicine.

drug-discovery clinical-trial target-discovery fibrosis

Original work: Nature
Announced: Insilico
Challenge: none linked

Novelty check, caveats & sources

Novelty check

AI-generated molecules had reached the clinic before, and AI-nominated targets had been published before, but this is the first randomised placebo-controlled efficacy signal for a compound where both the target and the molecule came from generative systems. TNIK's role in fibrosis was not an established target hypothesis when it was nominated.

Caveats

Phase 2a is small, short and exploratory: 71 patients over 12 weeks, single-country sites, not powered for efficacy, with FVC change over 12 weeks not a registrational endpoint. The sponsor designed, ran, analysed and published the trial. "AI-discovered" covers target selection and generative chemistry; the medicinal chemistry, preclinical work and trial conduct were conventional. A Phase 3 was subsequently initiated, which does not retrospectively strengthen this readout.

Original work

NatureNature Medicine: A generative AI-discovered TNIK inhibitor for idiopathic pulmonary fibrosis↗

Announcement

InsilicoInsilico Medicine: positive topline results of ISM001-055↗

Google DeepMind

2025-05-14

Independently checked Search scaffold

Model: AlphaEvolve (Gemini-based)
Field: computer-science
Posed: 1969 · open 56 yrs

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.

algorithms linear-algebra alphaevolve

Original work: DeepMind
Announced: DeepMind
Media: IEEE Spectrum
Commentary: Wikipedia
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Strassen (1969) and subsequent literature exhaustively catalogued; 49 was the standing record for complex-valued 4×4. Confirmed new.

Caveats

Applies to complex-valued matrices specifically. Practical speedup is limited; the significance is theoretical. Related follow-up work by others has explored rank-23 schemes for 3×3.

Original work

DeepMindAlphaEvolve paper (PDF)↗

Announcement

DeepMindAlphaEvolve↗

Media coverage

IEEE SpectrumIEEE Spectrum↗

Independent commentary

WikipediaAlphaEvolve↗

Community discussion

Hacker NewsAlphaEvolve announcement↗Hacker NewsAlphaEvolve independently discovered a novel matrix-multiplication algorithm↗

Google DeepMind

2025-05-14

Independently checked Search scaffold

Model: AlphaEvolve (Gemini-based)
Field: mathematics
Posed: 1694 · open 331 yrs

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.

geometry sphere-packing alphaevolve

Original work: DeepMind
Announced: DeepMind
Media: IEEE Spectrum
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Kissing number bounds are well catalogued per dimension; the 11D improvement was checked against the standing record.

Caveats

A lower-bound improvement via explicit construction, not a resolution of the problem. The 20% improvement rate means most of the 50+ problems saw no advance.

Original work

DeepMindAlphaEvolve paper (PDF)↗

Announcement

DeepMindAlphaEvolve↗

Media coverage

IEEE SpectrumAlphaEvolve Tackles Kissing Problem↗

Community discussion

Hacker NewsAlphaEvolve announcement↗

Google DeepMind

2025-05-14

Independently checked Search scaffold

Model: AlphaEvolve (Gemini-based)
Field: mathematics
Posed: 1955 · open 70 yrs

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.

analysis erdos alphaevolve

Original work: DeepMind
Announced: DeepMind
Commentary: Wikipedia
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The minimum-overlap constant and the autocorrelation inequalities have well-tracked records. AlphaEvolve's values were compared against the standing bounds and confirmed to improve them.

Caveats

The improvements are marginal in magnitude, and both were improved again by other automated systems in 2026. As with the other AlphaEvolve results, a human-designed evaluator and search loop did the selecting.

Original work

DeepMindAlphaEvolve paper (PDF)↗

Announcement

DeepMindAlphaEvolve↗

Independent commentary

WikipediaMinimum overlap problem↗

Community discussion

Hacker NewsAlphaEvolve announcement↗

FutureHouse

2025-05-01

Claimed AI-led

Model: Robin (multi-agent)
Field: biology

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.

drug-discovery ophthalmology needs-verification

Media: Turing Post
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Not independently audited by this registry at time of entry. Novelty check pending.

Caveats

Lab-announced. No independent verification located. A candidate treatment is many years and several trial phases from being a treatment. Held at 'claimed' until outside confirmation.

Media coverage

Turing Post12 AI Co-Scientists of 2026↗

Sakana AI

2025-03-12

Author verified AI-led

Model: The AI Scientist-v2
Field: computer-science

A fully machine-generated paper passed workshop peer review #

One of three end-to-end AI-generated manuscripts submitted to an ICLR 2025 workshop averaged 6.33 from reviewers and would have been accepted; the authors withdrew it, and the bar cleared was a workshop track, not the main conference.

The AI Scientist-v2 generates a hypothesis, writes and runs the experiments through agentic tree search, and produces the manuscript, figures and related work without human editing. Sakana submitted three such papers to the ICLR 2025 workshop "I Can't Believe It's Not Better", with the knowledge and cooperation of the workshop organisers and ICLR leadership, and agreed in advance to withdraw anything accepted. One paper, on whether an explicit compositional regularisation term improves compositional generalisation, scored 6.33 and cleared the bar.

autonomous-research peer-review agents contested

Original work: GitHub
Announced: Sakana AI
Challenge: TechCrunch

Novelty check, caveats & sources

Novelty check

Machine-written text had passed review before in the form of nonsense-generator stings (SCIgen, 2005), which tested review rather than produced research. The claim here is different: an autonomous pipeline produced a real experimental paper that reviewers rated acceptable. Sakana's own write-up is the source for the process, and the code and submitted manuscripts are public.

Caveats

Workshop tracks accept a far higher share of submissions than the main conference, and Sakana says so itself; the company also notes the accepted paper contains a citation error and that its own reviewers judged the work below the main-conference bar. The paper's scientific content is a negative result: the proposed regularisation did not help. Reviewers were not told which submissions were machine-generated, but the experiment ran with organiser consent, so this is not a blind test of peer review at scale. Humans chose the venue and selected which generated papers to submit, which caps autonomy at ai-led.

Original work

GitHubSakanaAI/AI-Scientist-ICLR2025-Workshop-Experiment (manuscripts and reviews)↗

Announcement

Sakana AIThe AI Scientist generates its first peer-reviewed publication↗

Challenge

TechCrunchSakana claims its AI paper passed peer review (it's more nuanced than that)↗

Google

2025-02-19

Author verified AI-assisted

Model: AI Co-Scientist (Gemini 2.0 multi-agent)
Field: biology

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.

hypothesis-generation microbiology multi-agent

Original work: bioRxiv
Media: Turing Post
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The AMR mechanism proposed had reportedly been independently arrived at by a human group whose work was unpublished at the time, which complicates the novelty claim.

Caveats

Hypothesis generation with human-run validation, not autonomous discovery. Independent replication outside the collaborating labs is limited. Graded conservatively.

Original work

bioRxivAI mirrors experimental science to uncover a novel mechanism of gene transfer↗

Media coverage

Turing Post12 AI Co-Scientists of 2026↗

Institute for Protein Design, University of Washington

2025-02-13

Peer reviewed Search scaffold

Model: RFdiffusion with PLACER ensemble scoring
Field: chemistry

Enzymes with working catalytic machinery designed from scratch #

Diffusion-based protein design produced serine hydrolases with catalytic efficiencies up to 2.2 × 10⁵ M⁻¹s⁻¹ on five folds unlike any natural serine hydrolase, with crystal structures matching the design models to under 1 Å.

An enzyme needs more than the right shape: its active site has to stay organised at every step of the reaction, which is where designed enzymes have historically failed. The team generated backbones with RFdiffusion from a minimal active-site description, then used an ensemble-generation network to check that the catalytic geometry held along the whole reaction coordinate, keeping only designs that passed. The resulting hydrolases approach natural catalytic efficiency on folds not found among natural serine hydrolases, and the crystal structures match the designs closely. Published in Science.

WithAnna Lauko, David Baker

protein-design enzyme-design rfdiffusion catalysis

Original work: Science
Announced: Baker Lab
Challenge: none linked

Novelty check, caveats & sources

Novelty check

De novo enzyme design dates to the 2000s (Kemp eliminases, retro-aldolases), but designed enzymes were typically orders of magnitude slower than natural ones and needed directed evolution to become useful. The advance is reaching this efficiency with multi-step catalytic machinery by design rather than by evolution.

Caveats

Serine hydrolases are a comparatively tractable target with a well-understood catalytic triad; the result does not generalise automatically to harder chemistry. Efficiencies remain below the best natural hydrolases. The per-round success rate is low and the paper reports the screening funnel. The reaction, the active-site description and the assays were human-specified, which is why autonomy is search-scaffold.

Original work

ScienceComputational design of serine hydrolases↗

Announcement

Baker LabGenerating new enzymes with complex active sites↗

EvolutionaryScale

2025-01-16

Peer reviewed AI-led

Model: ESM3 (98B)
Field: biology

A working fluorescent protein generated by a language model #

ESM3 designed esmGFP, a bright green fluorescent protein sharing only 58% of its sequence with the closest known natural fluorescent protein, a distance the authors estimate at over 500 million years of natural evolution.

ESM3 is a masked language model over protein sequence, structure and function jointly. Prompted with the residues that form the GFP chromophore and little else, and run through iterative generation, it produced candidates that were synthesised and assayed in the lab. esmGFP fluoresces at brightness comparable to natural GFPs while differing at 96 of 229 positions from its nearest natural relative. Published in Science.

WithAlexander Rives, Tom Sercu

protein-design generative-biology fluorescent-protein

Original work: Science
Announced: EvolutionaryScale
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Engineered GFP variants are routine but sit a handful of mutations from a natural template, and directed evolution moves in small steps. A functional fluorescent protein this far from any known sequence had not been reported, and the paper includes the expression, spectra and brightness measurements rather than a prediction alone.

Caveats

The 500-million-year figure is an inference from a sequence-divergence-to-time calibration, not a measurement, and has been criticised as a marketing frame. esmGFP was one hit from a generated and screened set; the paper reports the funnel. The design goal and the chromophore constraint were supplied by humans. No independent re-synthesis of esmGFP by an unaffiliated lab was on record when this entry was written.

Original work

ScienceSimulating 500 million years of evolution with a language model↗

Announcement

EvolutionaryScaleESM3 release↗

Microsoft Research

2025-01-16

Disputed Search scaffold

Model: MatterGen
Field: materials

Generative model designs crystals to order; its flagship synthesis turned out to be a known compound #

MatterGen generates crystal structures conditioned on target properties, and its headline experimental validation was later shown to match a compound reported in 1972 that sits in the model's own training data.

MatterGen is a diffusion model over crystal structures (atom types, coordinates and lattice jointly), trained on about 608,000 stable materials from the Materials Project and Alexandria, and fine-tunable to condition on a target property. Conditioned on a bulk modulus of 200 GPa it proposed a structure that collaborators at the Shenzhen Institutes of Advanced Technology synthesised, measuring 169 GPa, within 20% of the specification. Published in Nature.

materials crystal-structure diffusion-model contested

Original work: Nature GitHub
Announced: Microsoft
Challenge: Materials Horizons

Novelty check, caveats & sources

Novelty check

Generative models for crystals existed (CDVAE, and screening pipelines like GNoME); the contribution claimed is property-conditioned generation validated experimentally. The novelty question is precisely what is disputed below: whether the synthesised compound was new.

Caveats

A published critique in Materials Horizons argues the synthesised disordered phase Ta₁⁄₃Cr₂⁄₃O₂ is the same material as Ta₁⁄₂Cr₁⁄₂O₂ reported in 1972, that this compound is present in MatterGen's training set, and that its composition differs from the reported TaCr₂O₆, i.e. the flagship validation recovered a known material rather than a new one. The generative method itself is not refuted; the disputed part is the experimental novelty claim, and the entry is graded on the strength of that published objection. This registry keeps entries like this one rather than removing them.

Independent checks

Materials Horizons: Continued challenges in high-throughput materials predictions: disputed the novelty of the synthesised compound; identified it as present in the training data · link ↗

Original work

NatureA generative model for inorganic materials design↗GitHubMatterGen code and model weights↗

Announcement

MicrosoftMicrosoft Research: MatterGen, a new paradigm of materials design with generative AI↗

Challenge

Materials HorizonsMatterGen predicts compounds from the training dataset↗

Google DeepMind / Google Quantum AI

2024-11-20

Peer reviewed AI-led

Model: AlphaQubit
Field: physics

A neural decoder that identifies quantum errors more accurately than hand-designed methods #

A transformer trained on Google's Sycamore surface-code data cut decoding errors by 6% against tensor-network decoding and 30% against correlated matching, the best reported accuracy at the time.

A quantum error-correcting code produces a stream of syndrome measurements; a decoder has to infer from them which errors actually occurred. Hand-designed decoders assume a simplified noise model, whereas AlphaQubit is a transformer trained first on simulated data and then fine-tuned on hundreds of millions of real syndrome samples from Sycamore, so it can learn the device's actual correlated noise, leakage and crosstalk. It beat both the accuracy-oriented tensor-network decoder and the fast matching decoder, and held up in simulation to distance-11 codes. Published in Nature.

quantum-computing error-correction transformer

Original work: Nature
Announced: Google
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Machine-learning decoders had been proposed for years but had not beaten the best classical decoders on real hardware data at scale. The result is a decoder that does, on a specific processor.

Caveats

Accuracy, not speed: AlphaQubit is far slower than matching decoders and does not run inside the real-time budget a fault-tolerant machine needs, which the paper states. It is trained per device on that device's data, so it does not transfer for free. Scaling behaviour beyond the tested code distances is open. This improves a component of error correction; it does not itself demonstrate a fault-tolerant computation.

Original work

NatureLearning high-accuracy error decoding for quantum processors↗

Announcement

GoogleAlphaQubit, research on quantum error correction↗

FlyWire Consortium (Princeton, MRC LMB, Cambridge, Vermont)

2024-10-02

Peer reviewed AI-assisted

Model: Automated electron-microscopy segmentation networks
Field: neuroscience

Complete wiring diagram of an adult fruit-fly brain #

Machine segmentation of an electron-microscopy volume, corrected by a large community of proofreaders, produced the first synapse-level map of an entire adult brain: 139,255 neurons and roughly 50 million synapses.

A female Drosophila brain was sliced into about 7,000 sections and imaged by electron microscopy, producing a volume no team could trace by hand. Neural networks segmented the neurons automatically; more than 200 labs and a crowd of proofreaders then corrected the segmentation over several years and annotated over 8,000 cell types. Simulations built directly on the resulting wiring diagram predicted which neurons drive feeding and grooming, and the predictions held up experimentally. Published as a Nature package in October 2024.

WithSebastian Seung, Mala Murthy, Gregory Jefferis

connectome electron-microscopy segmentation drosophila

Original work: Nature FlyWire
Announced: NIH
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Complete connectomes existed for C. elegans (302 neurons, 1986) and the Drosophila larva (3,016 neurons, 2023). This one is roughly 45 times larger than the previous largest complete connectome, and automated segmentation is what made that scale reachable at all.

Caveats

Automated segmentation alone was not accurate enough: the result required years of human proofreading, which is why autonomy is graded ai-assisted rather than ai-led. Neurotransmitter identity is predicted rather than measured for most connections, and gap junctions and neuromodulation are not fully captured. It is one individual's brain, and a wiring diagram is not by itself an explanation of behaviour.

Original work

NatureNeuronal wiring diagram of an adult brain↗FlyWireFlyWire (data and explorer)↗

Announcement

NIHComplete wiring map of an adult fruit fly brain↗

Google DeepMind

2024-07-25

Independently checked AI-led

Model: AlphaProof + AlphaGeometry 2
Field: mathematics

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.

olympiad lean formalization benchmark

Original work: Nature
Announced: DeepMind
Media: Unite.AI
Challenge: none linked

Novelty check, caveats & sources

Novelty check

These are competition problems with published official solutions, so the achievement is a capability milestone (solving hard, known-answer problems under near-competition conditions) rather than a new mathematical result. The registry records it as such.

Caveats

Problems were hand-translated into formal Lean statements by people before AlphaProof attempted them, a real human contribution beyond posing the question, so autonomy is graded conservatively. AlphaProof also took far longer than the human time limit on some problems. This is benchmark performance on solved problems, not a discovery.

Independent checks

Timothy Gowers & Joseph Myers (competition-style grading): 28/42, silver-medal standard · link ↗

Original work

NatureOlympiad-level formal mathematical reasoning with reinforcement learning↗

Announcement

DeepMindAI achieves silver-medal standard solving IMO problems↗

Media coverage

Unite.AIHow AlphaProof and AlphaGeometry 2 achieved silver-medal standard↗

Community discussion

Hacker NewsAI solves IMO problems at silver-medal level↗

Video explainers

AlphaProof and AlphaGeometry 2 achieve a silver-medal score at the IMO, explainedElvis Saravia (DAIR.AI) YouTube ↗

Nothing loads from YouTube until you press play.

Google DeepMind / Isomorphic Labs

2024-05-08

Peer reviewed AI-led

Model: AlphaFold 3
Field: biology

Joint structure prediction for proteins, nucleic acids and ligands (AlphaFold 3)#

A diffusion-based successor to AlphaFold predicts complexes spanning proteins, DNA, RNA, small molecules and ions in a single model, with large accuracy gains over the specialised docking tools used for each case.

AlphaFold 2 predicted the fold of a protein chain; drug discovery mostly needs the structure of that protein bound to something else. AlphaFold 3 replaces the structure module with a diffusion model operating directly on atom coordinates, which lets one network cover protein–ligand, protein–nucleic-acid and antibody–antigen complexes. Reported accuracy substantially exceeds specialised docking tools on protein–ligand benchmarks. Published in Nature.

WithJohn Jumper, Max Jaderberg

protein-structure drug-discovery alphafold diffusion-model

Original work: Nature GitHub
Announced: Google
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Docking and complex prediction had decades of specialised tools (AutoDock, RoseTTAFold All-Atom, and AlphaFold-Multimer for protein assemblies). The contribution is one model spanning molecule types at higher accuracy, not a new biological result; the structures it predicts are natural ones.

Caveats

At publication neither code nor weights were released, only a rate-limited web server, which drew an open letter from over a thousand researchers about reproducibility; weights for academic use followed in November 2024. Accuracy on antibody–antigen complexes and some nucleic-acid targets is far below the headline figures, and the model can produce confidently wrong hallucinated structure in disordered regions. Predictions are hypotheses, not measurements.

Original work

NatureAccurate structure prediction of biomolecular interactions with AlphaFold 3↗GitHubAlphaFold 3 code (google-deepmind/alphafold3)↗

Announcement

GoogleGoogle DeepMind and Isomorphic Labs introduce AlphaFold 3↗

Princeton University / PPPL / DIII-D National Fusion Facility

2024-02-21

Peer reviewed Search scaffold

Model: Deep reinforcement learning controller over a learned plasma model
Field: physics

Reinforcement learning steers a tokamak away from tearing instabilities #

A controller trained on past DIII-D shots forecast tearing-mode instabilities up to 300 ms ahead and adjusted the plasma in real time to avoid them, holding high-performance conditions that would otherwise have collapsed.

Tearing modes break up the magnetic surfaces confining a fusion plasma and can end a discharge. Existing approaches suppress them once they appear; this one predicts them. A network trained on past DIII-D discharges estimates the instability probability, and a reinforcement-learning policy trained against a learned plasma model adjusts beam power and plasma shape to keep that probability low while holding pressure high. It was tested live on DIII-D, not only in simulation. Published in Nature.

WithJaemin Seo, Egemen Kolemen

fusion plasma-control reinforcement-learning tokamak

Original work: Nature
Announced: Princeton
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Distinct from the 2022 DeepMind–TCV work already in this registry, which learned magnetic shape control rather than instability avoidance. Tearing-mode prediction from machine learning had been published before; closing the loop so the controller acts on the prediction during a live shot is the new part.

Caveats

Demonstrated on one machine in specific scenarios. A data-driven controller trained on DIII-D discharges has no guarantee of transferring to another tokamak, still less to ITER-scale burning plasma where the training data does not exist. Tearing modes are one disruption pathway among several. The physics model, actuators and safety limits are human-designed; the policy operates inside them.

Original work

NatureAvoiding fusion plasma tearing instability with deep reinforcement learning↗

Announcement

PrincetonPrinceton Engineering: Engineers use AI to wrangle fusion power for the grid↗

Google DeepMind

2024-01-17

Peer reviewed Search scaffold

Model: AlphaGeometry
Field: mathematics

Olympiad geometry solved without human demonstrations #

A language model trained purely on synthetic data, paired with a symbolic deduction engine, solved 25 of 30 olympiad geometry problems against 10 for the previous best automated system and 25.9 for the average human gold medallist.

Geometry proofs stall when they need an auxiliary construction, an extra point or line that is not in the problem statement. AlphaGeometry pairs a symbolic deduction engine, which exhausts what follows mechanically, with a language model that proposes constructions when deduction runs dry. The model was trained on 100 million synthetic proofs generated from random diagrams, with no human proof data, and its output is a symbolic proof that the deduction engine checks. Published in Nature.

WithTrieu Trinh, Thang Luong

olympiad geometry neuro-symbolic benchmark

Original work: Nature GitHub
Announced: DeepMind
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Automated geometry provers date to Wu's method in the 1970s and to GEX/Java Geometry Expert; the prior state of the art solved 10 of the 30 benchmark problems. The benchmark is IMO geometry problems from 2000–2022 with known solutions, so the contribution is the method and the score, not a new theorem.

Caveats

Benchmark performance on solved problems, not a discovery. The domain is narrow: plane geometry expressible in the system's formal language, which excludes problems involving inequalities or variable numbers of points, and the benchmark set was filtered to what the language can state. Proof steps are machine-checked by the deduction engine, which is what carries the confidence; the peer-reviewed grade reflects Nature review of the system and results.

Original work

NatureSolving olympiad geometry without human demonstrations↗GitHubgoogle-deepmind/alphageometry (code)↗

Announcement

DeepMindAlphaGeometry, an olympiad-level AI system for geometry↗

Carnegie Mellon University

2023-12-20

Peer reviewed AI-led

Model: GPT-4 (Coscientist agent)
Field: chemistry

A language-model agent that planned and ran chemistry experiments on lab robots #

Coscientist, driven by GPT-4 with web search, documentation search, code execution and lab automation, designed and executed palladium-catalysed cross-coupling reactions on real robotic hardware from a one-line goal.

Given "perform Suzuki and Sonogashira reactions", the agent searched the literature to identify the chemistry, read the hardware documentation for an API it had not seen, wrote the control code, located the reagents on the plate from a UV-Vis reading, and ran the reactions on a liquid handler. The paper reports six tasks in total, including reaction optimisation under Bayesian search. Published in Nature.

WithDaniil Boiko, Robert MacKnight, Gabe Gomes

lab-automation agents cross-coupling self-driving-lab

Original work: Nature NIH PMC GitHub
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Robotic synthesis platforms and automated reaction optimisation predate this (Cronin's mobile robotic chemist, Nature 2020, among others). What was new is a general-purpose language model doing the planning, tool selection and code generation across unfamiliar hardware from a natural-language goal, rather than executing a human-written protocol.

Caveats

The chemistry performed is textbook cross-coupling: the finding is about autonomy, not about a new compound or reaction. The paper's own safety section shows the agent could be steered toward hazardous syntheses and the authors call for safeguards. Humans set up the hardware, reagents and safety envelope, and the tasks were chosen to be within the platform's reach.

Original work

NatureAutonomous chemical research with large language models↗NIH PMCPubMed Central full text↗GitHubCoscientist data and reference implementation↗

MIT / Broad Institute / Harvard

2023-12-20

Peer reviewed Search scaffold

Model: Ensembles of graph neural networks with substructure attribution
Field: chemistry

A new structural class of antibiotic candidates against MRSA #

Graph neural networks trained on 39,312 assayed compounds and applied to 12 million molecules surfaced a chemical class active against MRSA in mice, with the substructures driving each prediction made explicit rather than left opaque.

The team measured antibiotic activity and human-cell cytotoxicity for 39,312 compounds, trained network ensembles on that data, and predicted both properties for over 12 million molecules. Rather than reading off top scores, they extracted the chemical substructures the models were keying on, which let them pick a class rather than isolated hits. Two lead compounds cleared MRSA infection in mouse models, topically and systemically, and appear to kill by collapsing the electrochemical gradient across the bacterial membrane. Published in Nature.

WithFelix Wong, Erica Zheng, James Collins

antibiotics graph-neural-network explainability mrsa

Original work: Nature
Media: ScienceDaily
Challenge: none linked

Novelty check, caveats & sources

Novelty check

This is the same group's follow-up to the 2020 halicin work and to abaucin (2023); the new element is selecting a structural class via model interpretation instead of screening for individual hits. "New structural class" is a claim about scaffold novelty relative to clinical antibiotics, checked against known antibiotic chemotypes in the paper.

Caveats

These are candidates, not drugs: mouse models only, with no clinical development at the time of this entry. The mechanism, disrupting membrane potential, is the same one halicin uses, so the novelty is structural rather than mechanistic, and membrane-active compounds carry a known mammalian-toxicity risk. The screening library, assays and interpretation were human-run; the model scored and explained.

Original work

NatureDiscovery of a structural class of antibiotics with explainable deep learning↗

Media coverage

ScienceDailyUsing AI, researchers identify a new class of antibiotic candidates↗

Google DeepMind

2023-12-14

Peer reviewed Search scaffold

Model: FunSearch (PaLM 2 / Codey)
Field: mathematics
Posed: 1970 · open 53 yrs

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.

combinatorics cap-set funsearch historic-first

Original work: Nature GitHub
Announced: DeepMind
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Cap set bounds are a well-tracked literature; the constructions were confirmed to exceed the standing record at publication.

Caveats

The LLM proposes; a human-designed evaluator and search loop does the selecting. Calling this 'the AI discovered it' overstates the model's role, though the discovery is real.

Original work

NatureMathematical discoveries from program search with LLMs↗GitHubFunSearch code and discovered programs↗

Announcement

DeepMindFunSearch↗

Community discussion

Hacker NewsFunSearch makes new discoveries in mathematical sciences↗

Google DeepMind

2023-12-14

Peer reviewed Search scaffold

Model: FunSearch (PaLM 2 / Codey)
Field: computer-science
Posed: 1971 · open 52 yrs

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.

algorithms heuristics funsearch

Original work: Nature GitHub
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Compared against best-fit and first-fit families and published heuristics; improvements are empirical on tested distributions.

Caveats

An empirical improvement on benchmark distributions, not a proved worst-case bound.

Original work

NatureMathematical discoveries from program search with LLMs↗GitHubFunSearch code and discovered programs↗

Community discussion

Hacker NewsFunSearch makes new discoveries in mathematical sciences↗

Google DeepMind

2023-11-29

Disputed Search scaffold

Model: GNoME (graph neural network)
Field: materials

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.

materials crystal-structure graph-neural-network contested

Original work: Nature GitHub
Announced: DeepMind
Challenge: The Register

Novelty check, caveats & sources

Novelty check

Stable-material prediction builds on the Materials Project and OQMD convex-hull databases. The dispute below is precisely about how much of GNoME's set is genuinely new relative to those existing catalogues.

Caveats

Substantive objections were raised and remain unresolved. Cheetham and Seshadri, reviewing the release, found 'scant evidence for compounds that fulfil the trifecta of novelty, credibility and utility,' noting that many entries are minor substitutional variants, radioactive, or otherwise unlikely to be useful. Stability here means a DFT convex-hull prediction, not experimental synthesis; the headline counts are predicted, not made.

Independent checks

Cheetham & Seshadri (critical review): disputed the novelty and utility of most predicted compounds · link ↗

Original work

NatureScaling deep learning for materials discovery↗GitHubGNoME models, DFT data and 380k predicted structures↗

Announcement

DeepMindMillions of new materials discovered with deep learning↗

Challenge

The RegisterBoffins deem DeepMind's material discoveries shallow↗

Community discussion

The Registerchemists dispute DeepMind's AI materials discoveries↗

Lawrence Berkeley National Laboratory

2023-11-29

Disputed AI-led

Model: A-Lab (ML planning + robotics)
Field: materials

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.

materials autonomous-lab synthesis contested

Original work: Nature
Challenge: The Register

Novelty check, caveats & sources

Novelty check

Targets were drawn from computed stability databases. The contested question is whether the synthesised phases were correctly identified and genuinely new, rather than known phases or misindexed results.

Caveats

A detailed critique led by Robert Palgrave argued that many of the 41 claimed compounds were misidentified from the X-ray data, in several cases likely known phases, mixtures, or amorphous products rather than the claimed novel crystals. It is the identification step, not the automation, that is disputed; the autonomy claim itself is not the weak point. A 2026 Author Correction from the team re-analysed the diffraction data and clarified that 'novel' was meant as new to their prediction platform rather than necessarily new to science.

Independent checks

Palgrave et al. (analysis of the reported diffraction data): disputed the identification of most claimed new compounds · link ↗

Authors' correction (Nature, 2026): re-analysed diffraction data; clarified 'novel' meant new to the platform, not to science · link ↗

Original work

NatureAn autonomous laboratory for the accelerated synthesis of inorganic materials↗

Challenge

The RegisterBoffins deem DeepMind's material discoveries shallow↗

Community discussion

The Registerchemists dispute DeepMind's AI materials discoveries↗

Google DeepMind

2023-11-14

Peer reviewed AI-led

Model: GraphCast
Field: climate

Medium-range weather forecasts from a graph neural network beat the operational physics model #

GraphCast produced more accurate 10-day forecasts than ECMWF's HRES on roughly 90% of the evaluated variable and lead-time combinations, in under a minute on a single TPU against hours on a supercomputer.

GraphCast takes the two most recent global atmospheric states and predicts the next state six hours ahead on a roughly 0.25° grid, applied repeatedly to reach ten days. It is trained on ERA5 reanalysis rather than on the equations of motion, and it beat HRES, the operational gold standard, on the large majority of evaluated variables, rising to almost all of them within the troposphere. It also flagged severe weather events, including cyclone tracks, earlier than the physics model despite never being trained to look for them. Published in Science, with code and weights released.

WithRemi Lam, Peter Battaglia

weather forecasting graph-neural-network

Original work: Science GitHub
Announced: DeepMind
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Machine-learning weather models existed before (FourCastNet, Pangu-Weather), and Pangu had already reported beating HRES on some measures. GraphCast's contribution is the breadth of the win across variables and lead times, at operational resolution, with public code. That is what moved national weather services to adopt learned models.

Caveats

GraphCast is trained on ECMWF reanalysis and initialised from ECMWF analyses, so it depends on the physics-based system it is measured against rather than replacing it. Deterministic models trained on a mean-squared-error objective blur fine structure and underestimate extremes such as peak cyclone intensity. It has no conservation guarantees and cannot forecast anything outside its trained variables. Later ensemble models such as GenCast address part of this.

Original work

ScienceLearning skillful medium-range global weather forecasting↗GitHubGraphCast code and weights (google-deepmind/weathernext)↗

Announcement

DeepMindGraphCast, AI model for faster and more accurate global weather forecasting↗

Google DeepMind

2023-09-19

Peer reviewed AI-led

Model: AlphaMissense
Field: medicine

Pathogenicity predictions for 71 million human missense variants #

An AlphaFold-derived model classified 89% of all 71 million possible human missense variants as likely benign or likely pathogenic, against the roughly 0.1% that carry a clinical classification today.

AlphaMissense fine-tunes AlphaFold's structural representation on human and primate variant frequency data, so it learns which substitutions natural selection tolerates without being trained on clinical labels. Applied across 19,233 canonical human proteins it scored every possible single amino-acid change, calling 57% likely benign and 32% likely pathogenic. The full catalogue and the model code were released publicly. Published in Science.

genomics variant-effect clinical-genetics

Original work: Science Nature GitHub
Announced: DeepMind
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Variant-effect predictors are a crowded field (SIFT, PolyPhen-2, EVE, CADD). The contribution is proteome-wide coverage at state-of-the-art benchmark accuracy without training on clinical annotations, which is what makes the predictions usable where no clinical data exists.

Caveats

These are predictions, not diagnoses, and DeepMind says so: ACMG/AMP guidance treats computational evidence as supporting rather than standalone. Benchmarks have been criticised for circularity, since the model trains on population frequency and is evaluated partly against datasets encoding related signals. Calibration varies by gene, and a "likely pathogenic" call on a variant nobody has seen in a patient remains a hypothesis.

Original work

ScienceAccurate proteome-wide missense variant effect prediction with AlphaMissense↗NatureNature Biotechnology: Advancing missense variant pathogenicity prediction↗GitHubAlphaMissense predictions and code↗

Announcement

DeepMindA catalogue of genetic mutations to help pinpoint the cause of diseases↗

Google DeepMind

2023-06-07

Independently checked Search scaffold

Model: AlphaDev (AlphaZero-based)
Field: computer-science

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.

algorithms sorting reinforcement-learning deployed

Original work: Nature GitHub
Announced: DeepMind
Commentary: Wikipedia
Challenge: none linked

Novelty check, caveats & sources

Novelty check

The libc++ small-sort routines had been hand-optimised by compiler engineers for years. AlphaDev's shorter instruction sequences were reviewed against the standing implementations and confirmed to be improvements before being merged.

Caveats

The gains are on very short fixed-length inputs; asymptotic sorting complexity is unchanged, and the headline percentage speedups apply only to those small cases. The 'independent' grade rests on LLVM maintainers reviewing and merging the code, not on a formal proof of optimality.

Independent checks

LLVM libc++ maintainers (code review and merge): reviewed and merged into the standard sort library · link ↗

Original work

NatureFaster sorting algorithms discovered using deep reinforcement learning↗GitHubAlphaDev code and discovered sorting routines↗

Announcement

DeepMindAlphaDev discovers faster sorting algorithms↗

Independent commentary

WikipediaAlphaDev↗

Community discussion

Hacker NewsAlphaDev, faster sorting algorithms via deep RL↗

Video explainers

AlphaDev: Discovering Faster Sorting Algorithms with Reinforcement LearningAI for Good (ITU) YouTube ↗

Nothing loads from YouTube until you press play.

Google DeepMind

2022-10-05

Peer reviewed Search scaffold

Model: AlphaTensor (AlphaZero-based)
Field: computer-science
Posed: 1969 · open 53 yrs

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.

algorithms linear-algebra reinforcement-learning

Original work: Nature GitHub
Announced: DeepMind
Media: Quanta
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Fast matrix multiplication has an exhaustively catalogued literature going back to Strassen (1969) and Laderman (1976). AlphaTensor's schemes were checked against the standing per-size records; the 4×4 result over GF(2) was new at publication.

Caveats

The 4×4 improvement is specific to characteristic-2 arithmetic and the practical speedup is limited. Within about a week, Kauers and Moosbauer used a classical computer search to improve the 5×5 GF(2) case from AlphaTensor's 96 multiplications to 95, showing conventional methods remained competitive. 'Discovered' here means an RL search over decompositions, not an autonomous mathematical insight.

Independent checks

Kauers & Moosbauer (computer-algebra search): verified and shortly improved on the 5×5 case · link ↗

Original work

NatureDiscovering faster matrix multiplication algorithms with reinforcement learning↗GitHubAlphaTensor code and discovered algorithms↗

Announcement

DeepMindDiscovering novel algorithms with AlphaTensor↗

Media coverage

QuantaAI Reveals New Possibilities in Matrix Multiplication↗

Community discussion

Hacker NewsDiscovering novel algorithms with AlphaTensor↗Hacker NewsOn AlphaTensor's new matrix multiplication algorithms↗Hacker Newshuman search beats AlphaTensor's 5×5 result days later↗

Video explainers

How AI Discovered a Faster Matrix Multiplication AlgorithmQuanta Magazine YouTube ↗

AlphaTensor by DeepMind explainedYannic Kilcher YouTube ↗

Nothing loads from YouTube until you press play.

Google DeepMind

2022-02-16

Peer reviewed Search scaffold

Model: DeepMind RL controller
Field: physics

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.

physics fusion reinforcement-learning control

Original work: Nature
Announced: DeepMind EPFL
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Magnetic plasma control is normally built from many separately engineered controllers. A single RL-learned controller running on a real tokamak was new; the Nature paper documents the comparison against conventional control.

Caveats

Demonstrated on the TCV research tokamak, not a power-producing reactor, and the policy was trained in simulation before transfer to hardware. This is a control-engineering advance, not a solution to fusion energy. Independent groups have since extended RL plasma control to other machines.

Original work

NatureMagnetic control of tokamak plasmas through deep reinforcement learning↗

Announcement

DeepMindAccelerating fusion science through learned plasma control↗EPFLEPFL and DeepMind use AI to control plasmas for fusion↗

Community discussion

Hacker Newscontrolling the fusion plasma in a tokamak with reinforcement learning↗

Google DeepMind (with Oxford and Sydney)

2021-12-01

Peer reviewed AI-assisted

Model: Supervised networks with gradient-based attribution
Field: mathematics

Two theorems found by machine pattern-spotting in knot theory and representation theory #

Networks trained to predict one mathematical invariant from another, then probed for which inputs mattered, pointed mathematicians to a proved theorem linking a knot's signature to a new geometric quantity, and to structure behind the combinatorial invariance conjecture.

The recipe was to train a network to predict one invariant from another, then use attribution to see which inputs carried the signal, and hand that to a mathematician. In knot theory it led Marc Lackenby to define a new quantity, the natural slope of a knot, and to prove a theorem bounding the signature in terms of it. In representation theory it led Geordie Williamson to structure in Bruhat interval graphs bearing on the combinatorial invariance conjecture for Kazhdan–Lusztig polynomials. Published in Nature.

WithAlex Davies, Marc Lackenby, Geordie Williamson

knot-theory representation-theory conjecture-generation

Original work: Nature GitHub
Announced: Oxford
Challenge: arXiv

Novelty check, caveats & sources

Novelty check

Both theorems are new and neither had a prior form in the literature; both were proved conventionally by the human mathematicians after the models indicated where to look. The general idea of using computation to generate conjectures is old; what was new was the attribution step turning a black-box predictor into a usable hint.

Caveats

The mathematics was done by humans; the models indicated which relationships were worth studying, which is why autonomy is ai-assisted. Ernest Davis's review argues the "guiding human intuition" framing overstates the contribution and that the knot-theory signal was within reach of simpler statistical methods. The theorems themselves are not disputed.

Independent checks

Ernest Davis (critical review of the framing): theorems accepted; disputes how much the deep learning contributed · link ↗

Original work

NatureAdvancing mathematics by guiding human intuition with AI↗GitHubKnot theory and representation theory notebooks↗

Announcement

OxfordUniversity of Oxford: Machine learning helps mathematicians make new connections↗

Challenge

arXivErnest Davis: Deep Learning and Mathematical Intuition (review)↗

Google DeepMind

2021-07-15

Independently checked AI-led

Model: AlphaFold2
Field: biology
Posed: 1972 · open 49 yrs

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

protein-structure biology alphafold nobel-prize

Original work: Nature GitHub
Announced: DeepMind
Commentary: Nobel Prize
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Protein-structure prediction had been an open grand challenge for roughly fifty years, benchmarked every two years by the CASP assessment. AlphaFold2's CASP14 result was a discontinuous jump over all prior methods and is uncontested.

Caveats

AlphaFold predicts structures rather than determining them experimentally; outputs are computational hypotheses that can be wrong for disordered regions, alternative folds, point mutations, and many complexes. It predicts natural structures, not new biology on its own. The grade reflects the prediction step; the Nobel recognised the human-built method.

Independent checks

CASP14 blind assessment (independent assessors): accuracy competitive with experiment across most targets

Royal Swedish Academy of Sciences (2024 Nobel in Chemistry): awarded to Hassabis and Jumper for protein structure prediction · link ↗

Original work

NatureHighly accurate protein structure prediction with AlphaFold↗GitHubAlphaFold code (google-deepmind/alphafold)↗

Announcement

DeepMindAlphaFold↗

Independent commentary

Nobel PrizeChemistry 2024 press release↗

Tel Aviv University

2021-04-29

Independently checked Search scaffold

Model: Deep cross-entropy method (custom network)
Field: mathematics

Reinforcement learning refutes several conjectures in extremal combinatorics #

A neural network building graphs edge by edge under a cross-entropy search produced explicit counterexamples to several published conjectures in graph theory and extremal combinatorics.

Each conjecture was rewritten as a scoring function on graphs. A network proposes graphs one edge at a time, the top-scoring constructions are kept, and the network is retrained on them, so the search drifts toward whatever the conjecture says should be impossible. Among the conjectures refuted are a question of Brualdi and Cao on maximising permanents of pattern-avoiding matrices and several concerning adjacency and distance eigenvalues of graphs. The counterexamples are small finite graphs printed in the paper, so each can be checked by hand or by a few lines of code.

WithAdam Zsolt Wagner

combinatorics graph-theory counterexample reinforcement-learning

Original work: arXiv GitHub
Challenge: arXiv

Novelty check, caveats & sources

Novelty check

Computer search for combinatorial counterexamples predates this work: linear-programming and SAT-based refutations go back years, including Refuting conjectures in extremal combinatorics via linear programming (2019). What was new is the reinforcement-learning formulation and the specific conjectures, which were open at the time. The paper is widely treated as the origin of the "AI finds counterexamples" line of work.

Caveats

An arXiv preprint; no journal publication is listed on the arXiv record five years on. The refuted conjectures are individually modest (none is a named problem of the Erdős or Jacobian class), and several came from open-problem lists rather than headline literature. Autonomy is search-scaffold on the strictest reading: the human chose the conjectures, wrote the scoring function that encodes each one, and designed the search; the network only proposes graphs.

Independent checks

Roucairol & Cazenave, Monte Carlo search replication and extension: reproduced the refutations and found further counterexamples by different search · link ↗

Original work

arXivConstructions in combinatorics via neural networks↗GitHubWagner's cross-entropy code for the counterexamples↗

Challenge

arXivRefutation of Spectral Graph Theory Conjectures with Monte Carlo Search↗

MIT / Broad Institute

2020-02-20

Peer reviewed Search scaffold

Model: Directed message-passing graph neural network (Chemprop)
Field: medicine

Halicin, an antibiotic found by a neural network screening a compound library #

A graph neural network trained on 2,335 molecules picked halicin out of a repurposing library; it killed multidrug-resistant bacteria including Acinetobacter baumannii and Mycobacterium tuberculosis in vitro and cleared infections in mice.

The model was trained to predict growth inhibition of E. coli from structure alone, then applied to the Drug Repurposing Hub. Halicin, an abandoned diabetes candidate, scored highly despite being structurally unlike known antibiotics. It kills by dissipating the proton-motive force across the bacterial membrane, and the team could not evolve resistant E. coli over 30 days of serial passage. A follow-up screen of about 107 million molecules from ZINC15 produced eight further candidates. Published in Cell.

WithJonathan Stokes, Regina Barzilay, James Collins

antibiotics drug-repurposing graph-neural-network

Original work: Cell
Announced: MIT News
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Virtual screening long predates deep learning. What was new was a model surfacing a hit structurally distant from its training set, with a mechanism distinct from existing antibiotic classes, and the follow-through to efficacy in animals. Halicin itself was a known molecule; the discovery is of its antibacterial activity, not of the compound.

Caveats

Halicin had not entered clinical trials six years on, which is the usual fate of antibiotic leads and a reminder that discovery is not the bottleneck in this field. The model ranked compounds; the mechanism work, the animal studies and the interpretation are human. Membrane-disrupting antibacterials carry a known selectivity risk in mammals.

Original work

CellA deep learning approach to antibiotic discovery↗

Announcement

MIT NewsArtificial intelligence yields new antibiotic↗

Google Brain / University of Texas at Austin

2017-12-14

Peer reviewed Search scaffold

Model: Convolutional neural network (AstroNet)
Field: astronomy

An eighth planet around Kepler-90 found by a neural network #

A convolutional network re-examining Kepler light curves recovered transit signals the standard pipeline had ranked below threshold, yielding Kepler-90i and making Kepler-90 the first star besides the Sun known to host eight planets.

The network was trained on 15,000 previously vetted Kepler signals to separate genuine transits from false positives, then pointed at 670 stars already known to host multiple planets, searching the weak signals the automated pipeline had discarded. It surfaced Kepler-90i (about 30% larger than Earth, orbiting every 14.4 days, with a surface hot enough to rival Mercury) and Kepler-80g, which completes a five-planet resonant chain. Published in The Astronomical Journal.

WithChristopher Shallue, Andrew Vanderburg

exoplanets kepler transit-detection

Original work: IOP GitHub
Announced: NASA
Challenge: none linked

Novelty check, caveats & sources

Novelty check

Machine classification of Kepler transit candidates already existed in the pipeline (Autovetter, Robovetter). What was new was training a network to vet signals below the pipeline's detection threshold and getting confirmable planets out of the discard pile.

Caveats

The network vetted candidate signals; the transit search, the follow-up and the statistical validation were conventional. "First system with as many planets as ours" is a statement about what has been detected, not what exists. Detection is heavily biased toward close-in planets, and all of Kepler-90's known planets orbit within roughly Earth's distance from its star. The 670-star search produced two new planets in total.

Original work

IOPThe Astronomical Journal: Identifying Exoplanets with Deep Learning↗GitHubAstroNet: Kepler light-curve models (exoplanet-ml)↗

Announcement

NASAArtificial intelligence, NASA data used to discover eighth planet circling distant star↗

All findings in the registry, sortable by column.
			Model			Field
2026-08-01	Ten results in mathematics and theoretical computer science with Lean certificates	OpenAI	Astra	Formally verified	AI-led	mathematics
2026-07-22	Counterexample to the Dinitz–Garg–Goemans conjecture	Independent	GPT-5.6 Pro	Claimed	AI-led	computer-science
2026-07-20	Counterexamples to the Gaussian moments conjecture	Independent	GPT-5.6 Sol Pro + Claude Fable 5	Author verified	AI-led	mathematics
2026-07-20	Eight problems from the Kourovka Notebook solved and formalized in Lean	Harmonic	Aristotle	Formally verified	Autonomous	mathematics
2026-07-19	Counterexample to the Jacobian conjecture in dimension three	Anthropic	Claude Fable 5	Formally verified	Collaborative	mathematics
2026-07-14	Near-quadratic lower bound for derivative-free convex optimization	Independent	GPT-5.6 Sol Pro	Formally verified	AI-led	mathematics
2026-07-11	Counterexample to Grothendieck's question on finite flat group schemes	Independent	OpenAI Sol (construction); Claude Fable (Lean formalisation)	Formally verified	Collaborative	mathematics
2026-06-25	First Herculaneum scroll read end to end without unrolling it	Vesuvius Challenge	Community-developed ink-detection neural networks	Author verified	AI-assisted	archaeology
2026-06-17	Two kagome superconductors predicted by machine learning and confirmed in the lab	Aalto University / Rice University	Unknown	Peer reviewed	Search scaffold	materials
2026-05-21	Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs	Google DeepMind	AlphaProof Nexus (LLM + Lean)	Formally verified	Search scaffold	mathematics
2026-05-20	Disproof of the Erdős unit-distance conjecture	OpenAI	GPT-5 series reasoning model	Independently checked	AI-led	mathematics
2026-05-18	Phase 1 trial of a computationally designed pan-sarbecovirus vaccine	University of Cambridge / DIOSynVax	Unknown	Peer reviewed	AI-assisted	medicine
2026-01-15	Structure in Bruhat intervals of permutation groups	Google DeepMind	AlphaEvolve (Gemini-based)	Independently checked	Search scaffold	mathematics
2026-01-13	Erdős problem #728 resolved and formalized in Lean	OpenAI / Harmonic	GPT-5.2 Pro + Aristotle	Formally verified	Autonomous	mathematics
2025-11-20	Early science acceleration experiments with GPT-5	OpenAI	GPT-5	Peer reviewed	AI-assisted	computer-science
2025-11-03	AlphaEvolve across 67 problems: 20 improvements, 8 regressions	Google DeepMind	AlphaEvolve (Gemini-based)	Independently checked	Search scaffold	mathematics
2025-10-19	GPT-5 "solved 10 Erdős problems": it located existing solutions	OpenAI	GPT-5	Already known	Retrieval	mathematics
2025-09-25	Limits to black-box amplification in QMA, with the key step written by GPT-5	UT Austin / CWI Amsterdam	GPT-5 Thinking	Author verified	AI-assisted	computer-science
2025-09-17	New families of unstable singularities in fluid equations	Google DeepMind (with Brown, NYU and Stanford)	Physics-informed neural networks with Gauss–Newton optimisation	Author verified	Search scaffold	mathematics
2025-09-17	AI-generated bacteriophage genomes that replicate and kill bacteria	Arc Institute / Stanford University	Evo 1 and Evo 2	Peer reviewed	AI-led	biology
2025-09-11	Strong prime number theorem formalized in Lean by an autoformalization agent	Math, Inc.	Gauss (autoformalization agent)	Author verified	AI-assisted	mathematics
2025-08-01	Improved step-size bound in smooth convex optimization	OpenAI	GPT-5 Pro	Already known	AI-assisted	mathematics
2025-07-28	Machine-checked Lean proofs for five of six 2025 IMO problems	Harmonic	Aristotle	Formally verified	AI-led	mathematics
2025-07-21	Gold-medal standard at the 2025 International Mathematical Olympiad	Google DeepMind	Gemini Deep Think (advanced version)	Independently checked	AI-led	mathematics
2025-06-03	Phase 2a results for a drug whose target and molecule both came from AI	Insilico Medicine	PandaOmics (target) + Chemistry42 (molecule)	Peer reviewed	Search scaffold	medicine
2025-05-14	4×4 complex matrix multiplication in 48 scalar multiplications	Google DeepMind	AlphaEvolve (Gemini-based)	Independently checked	Search scaffold	computer-science
2025-05-14	Improved lower bound for the 11-dimensional kissing number	Google DeepMind	AlphaEvolve (Gemini-based)	Independently checked	Search scaffold	mathematics
2025-05-14	Improved bound for the Erdős minimum-overlap problem	Google DeepMind	AlphaEvolve (Gemini-based)	Independently checked	Search scaffold	mathematics
2025-05-01	Candidate treatment for dry age-related macular degeneration	FutureHouse	Robin (multi-agent)	Claimed	AI-led	biology
2025-03-12	A fully machine-generated paper passed workshop peer review	Sakana AI	The AI Scientist-v2	Author verified	AI-led	computer-science
2025-02-19	AI co-scientist hypotheses on antimicrobial resistance and liver fibrosis	Google	AI Co-Scientist (Gemini 2.0 multi-agent)	Author verified	AI-assisted	biology
2025-02-13	Enzymes with working catalytic machinery designed from scratch	Institute for Protein Design, University of Washington	RFdiffusion with PLACER ensemble scoring	Peer reviewed	Search scaffold	chemistry
2025-01-16	A working fluorescent protein generated by a language model	EvolutionaryScale	ESM3 (98B)	Peer reviewed	AI-led	biology
2025-01-16	Generative model designs crystals to order; its flagship synthesis turned out to be a known compound	Microsoft Research	MatterGen	Disputed	Search scaffold	materials
2024-11-20	A neural decoder that identifies quantum errors more accurately than hand-designed methods	Google DeepMind / Google Quantum AI	AlphaQubit	Peer reviewed	AI-led	physics
2024-10-02	Complete wiring diagram of an adult fruit-fly brain	FlyWire Consortium (Princeton, MRC LMB, Cambridge, Vermont)	Automated electron-microscopy segmentation networks	Peer reviewed	AI-assisted	neuroscience
2024-07-25	Silver-medal standard at the 2024 International Mathematical Olympiad	Google DeepMind	AlphaProof + AlphaGeometry 2	Independently checked	AI-led	mathematics
2024-05-08	Joint structure prediction for proteins, nucleic acids and ligands (AlphaFold 3)	Google DeepMind / Isomorphic Labs	AlphaFold 3	Peer reviewed	AI-led	biology
2024-02-21	Reinforcement learning steers a tokamak away from tearing instabilities	Princeton University / PPPL / DIII-D National Fusion Facility	Deep reinforcement learning controller over a learned plasma model	Peer reviewed	Search scaffold	physics
2024-01-17	Olympiad geometry solved without human demonstrations	Google DeepMind	AlphaGeometry	Peer reviewed	Search scaffold	mathematics
2023-12-20	A language-model agent that planned and ran chemistry experiments on lab robots	Carnegie Mellon University	GPT-4 (Coscientist agent)	Peer reviewed	AI-led	chemistry
2023-12-20	A new structural class of antibiotic candidates against MRSA	MIT / Broad Institute / Harvard	Ensembles of graph neural networks with substructure attribution	Peer reviewed	Search scaffold	chemistry
2023-12-14	New lower bound constructions for the cap set problem	Google DeepMind	FunSearch (PaLM 2 / Codey)	Peer reviewed	Search scaffold	mathematics
2023-12-14	Improved heuristics for online bin packing	Google DeepMind	FunSearch (PaLM 2 / Codey)	Peer reviewed	Search scaffold	computer-science
2023-11-29	Large-scale prediction of new stable crystalline materials (GNoME)	Google DeepMind	GNoME (graph neural network)	Disputed	Search scaffold	materials
2023-11-29	Autonomous laboratory reports solid-state synthesis of new inorganic compounds	Lawrence Berkeley National Laboratory	A-Lab (ML planning + robotics)	Disputed	AI-led	materials
2023-11-14	Medium-range weather forecasts from a graph neural network beat the operational physics model	Google DeepMind	GraphCast	Peer reviewed	AI-led	climate
2023-09-19	Pathogenicity predictions for 71 million human missense variants	Google DeepMind	AlphaMissense	Peer reviewed	AI-led	medicine
2023-06-07	Faster sorting routines discovered and merged into the LLVM C++ library	Google DeepMind	AlphaDev (AlphaZero-based)	Independently checked	Search scaffold	computer-science
2022-10-05	Faster matrix-multiplication algorithms found by reinforcement learning	Google DeepMind	AlphaTensor (AlphaZero-based)	Peer reviewed	Search scaffold	computer-science
2022-02-16	Deep reinforcement learning controls tokamak fusion plasma	Google DeepMind	DeepMind RL controller	Peer reviewed	Search scaffold	physics
2021-12-01	Two theorems found by machine pattern-spotting in knot theory and representation theory	Google DeepMind (with Oxford and Sydney)	Supervised networks with gradient-based attribution	Peer reviewed	AI-assisted	mathematics
2021-07-15	Accurate protein structure prediction across the known proteome (AlphaFold2)	Google DeepMind	AlphaFold2	Independently checked	AI-led	biology
2021-04-29	Reinforcement learning refutes several conjectures in extremal combinatorics	Tel Aviv University	Deep cross-entropy method (custom network)	Independently checked	Search scaffold	mathematics
2020-02-20	Halicin, an antibiotic found by a neural network screening a compound library	MIT / Broad Institute	Directed message-passing graph neural network (Chemprop)	Peer reviewed	Search scaffold	medicine
2017-12-14	An eighth planet around Kepler-90 found by a neural network	Google Brain / University of Texas at Austin	Convolutional neural network (AstroNet)	Peer reviewed	Search scaffold	astronomy

Evidence chain

Open longest before falling

Findings per year

By topic area

Browse by topic

Announced at the source

Also watched, nothing on record yet

Reference and discussion