What AI has
actually contributed

SOP_2 and SOP_3 theories shown to coincide#

The classes of SOP_2 and SOP_3 first-order theories are the same, answering a 2004 question of Džamonja and Shelah and collapsing the bottom of the SOP hierarchy to a single class.

Džamonja and Shelah introduced the tree configurations SOP_1 and SOP_2 in 2004 and asked whether either implication in the chain from SOP_3 to SOP_2 to SOP_1 reverses. Mutchnik answered the second, proving SOP_1 equals SOP_2, and the surviving half organised much of the subsequent NSOP_1 literature, with partial results by Conant, by Kaplan, Ramsey and Simon, and by Mutchnik. This five-page paper proves that SOP_2 implies SOP_3, the converse having been known from the start, which collapses the bottom of the hierarchy to a single class and carries consequences for Keisler-order maximality. The SOP_n hierarchy for n at least three is untouched, as is everything above it.

WithArtem Chernikov

Original work

arXiv↗

Commentary

VibeMathed↗

Challenge

none linked

Complete minimizer picture for Gamow's liquid drop model#

Balls uniquely minimize the Gamow liquid drop energy at every volume up to a sharp threshold of about 3.51, and above that threshold no minimizer exists, closing a gap that partial results had narrowed from both sides without meeting.

Gamow's liquid drop functional adds De Giorgi perimeter to a Coulomb repulsion term, and the central question in its literature is the fixed-volume minimization picture: for which volumes a minimizer exists, and whether it is the ball. This proves that balls uniquely minimize, up to translation and null sets, at every volume up to a threshold of 5 times 2 minus 2 to the two thirds, divided by 2 to the two thirds minus 1, roughly 3.51, and that above that threshold no minimizer exists at all. A corollary settles the minimal binding energy question of Frank and Lieb, identifying the infimum of energy per unit volume and the ball of volume 5/2 as the unique minimizer. The mechanism is a capacitary estimate sharpening an Agostiniani–Mazzieri monotonicity formula through Gauss–Bonnet, an improvement the authors note applies only to this particular weight and only in three dimensions.

WithOtis Chodosh, Matilde Gianocca

Original work

arXiv↗

Commentary

arXiv↗VibeMathed↗

Challenge

none linked

Proportion of zeta zeros on the critical line raised to 67.25%#

An unconditional proof that at least 67.25% of the nontrivial zeros of the Riemann zeta function are simple and lie on the critical line, up from a previous record of about 41.6%, with a machine-checked Lean formalization.

The Riemann hypothesis asserts every nontrivial zero lies on the critical line. Short of proving it, the standard measure of progress is the proportion of zeros known unconditionally to lie there: Selberg established a positive proportion, Levinson reached a third in 1974, Conrey two fifths in 1989, and the record had crept to roughly 41.6%. This work proves at least 3/2 - (1/sqrt 2)cot(1/sqrt 2) = 67.25...% of zeros are simple and on the line, and that at least 0.83625 of zeros are distinct. The decisive step combined the unconditional pair-correlation work of Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh with a 2000 paper of Bombieri, treating the whole function space at once with the quadratic form allowed to be non-diagonal rather than splitting it. The process is itself the record worth noting: the model was asked to attempt the Riemann hypothesis outright, with the mathematical choices left to it, and the bound improvement fell out of failing at that. It generated and discarded roughly 650 ideas in a first session; in a second it coordinated about 60 subagents which ran some 2,400 shell commands, wrote hundreds of scripts, checked numerically against known zeros and refereed one another. Two subagents developed the key ideas, thirteen fed them, thirty tried and failed, thirteen validated, two drafted the paper, across roughly 31 million output tokens in two Claude Code sessions. The model also proposed writing the result up, checked 54 arXiv papers for prior art, and recommended a human number theorist validate it.

WithJarred Sumner, Levent Alpöge, Ralph Furman, Eric Easley

Original work

Anthropic↗GitHub↗

Announced

Anthropic↗

Commentary

VibeMathed↗

Challenge

none linked

A 112-vertex counterexample to the Petersen coloring conjecture#

An explicit simple bridgeless cubic graph on 112 vertices admits no Petersen coloring, and hence no normal 5-edge-coloring, refuting a conjecture of Jaeger from 1985 with machine-checked UNSAT certificates.

Jaeger conjectured in 1985 that every bridgeless cubic graph admits a Petersen coloring: a map from its edges into the edges of the Petersen graph sending the three edges at each vertex to three edges meeting at a common vertex of the Petersen graph. Equivalently, every bridgeless cubic graph has a normal 5-edge-coloring. The conjecture implies both the Berge–Fulkerson conjecture and the 5-cycle-double-cover conjecture. This paper gives an explicit simple connected bridgeless cubic graph on 112 vertices, of girth five and edge and vertex connectivity three, with no such coloring; the graph is pinned by a SHA-256 digest in the theorem statement itself. Non-existence is established by direct SAT formulations, with CaDiCaL 3.0.1 returning UNSAT and drat-trim verifying the resulting DRAT proofs. A second, non-isomorphic counterexample of the same order is supplied. The implication runs one way, so Berge–Fulkerson and the 5-cycle-double-cover conjecture stay open; combined with a theorem of Ma, Mattiolo, Steffen and Wolf, one counterexample yields infinitely many.

WithBryce Putman

Original work

arXiv↗DOI↗

Commentary

Open Problem Garden↗VibeMathed↗

Challenge

none linked

Sendov's conjecture proved for every degree#

For every complex polynomial of degree at least two whose zeros all lie in the closed unit disk, each zero has a critical point of the polynomial within distance one, closing a question open since 1959.

Sendov's conjecture states that if every zero of a complex polynomial of degree n at least two lies in the closed unit disk, then every zero has a critical point within distance one. Degrees up to eight were settled piecemeal between 1969 and 1999, and Tao proved the conjecture for all sufficiently large degree in 2020 without specifying the threshold, which left the middle range open. Lech Mazur, working with GPT-5.6 Pro, produced an argument covering every degree along with a Lean development of roughly 90,000 lines. Terence Tao then digested the proof, describing it as remarkably elementary with no complex analysis used beyond the fundamental theorem of algebra, and formalized the entire argument himself in about 15,000 lines. He reports that the same argument resolves the Phelps–Rodriguez conjecture in full generality.

WithLech Mazur

Original work

ProofAtlas↗ProofAtlas↗

Commentary

Terence Tao↗VibeMathed↗

Challenge

none linked

Counterexamples to Schiffer's conjecture and the Pompeiu problem#

Infinitely many planar domains that are not balls admit a Neumann eigenfunction of the Laplacian that is constant on the boundary, disproving Schiffer's conjecture and, through a classical equivalence, the 1929 Pompeiu problem.

Pompeiu asked in 1929 whether a bounded domain over which some nonzero function integrates to zero under every rigid motion must be a ball. Schiffer's 1957 reformulation asks the same thing through Neumann eigenfunctions of the Laplacian that are constant on the boundary, and appears as Problem 80 on Yau's 1982 list; Williams proved the two formulations equivalent for simply connected domains in 1976. Cao-Labora and de Dios Pont construct infinitely many N-fold symmetric planar domains, with N large, that are not balls and carry such an eigenfunction. The strategy is to relax the problem so that N may be any real number, which corresponds to the Schiffer problem only at integers, apply bifurcation theory there, and show the size of the local bifurcation branch can be taken independently of N. Their Corollary 1.2 applies Williams' equivalence to the same domains, so a single construction settles both problems.

WithGonzalo Cao-Labora, Jaume de Dios Pont

Original work

arXiv↗GitHub↗

Commentary

Wikipedia↗VibeMathed↗

Challenge

none linked

Asymptotic degree-diameter problem resolved for fixed diameter#

The maximum order of a graph with maximum degree d and diameter k satisfies n_k(d)/d^k tending to 1 as d grows, for every fixed k, resolving the asymptotic form of a question open since 1978, with a Lean 4 formalization.

The Moore bound caps the order of a graph of maximum degree d and diameter k at roughly d^k. Whether that cap is asymptotically attainable for fixed diameter was open: Bannai and Ito had settled which exact Moore graphs exist, and constructions had approached the bound only for small diameters. This proves the limit of n_k(d)/d^k is 1 for every fixed k, with a companion lower bound on the edge variant and a tight asymptotic for the bipartite version. The paper carries an explicit tool and computational resource disclosure: GPT-5.6 Pro was used in exploratory brainstorming directed by the authors, who formulated the required parameter scale and proposed higher-rank spherical buildings as the geometric setting. The model suggested splitting complete flags into their odd- and even-rank subflags, initially in connection with the edge problem; that suggestion became the halved-flag construction carrying the main theorem, and the graph is named for it.

WithWouter Cames van Batenburg, Samuel Korsky

Original work

arXiv↗GitHub↗

Commentary

VibeMathed↗

Challenge

none linked

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

Optimal exponent relating sumsets and difference sets determined#

The least universal exponent c with |A+A|/|A| bounded by (|A-A|/|A|)^c for every finite integer set A is determined, settling the extremal question with a Lean 4 formalization.

For a finite set A of integers with at least two elements, the ratio of log(|A+A|/|A|) to log(|A-A|/|A|) measures how far sumset growth can outrun difference-set growth. Determining its largest possible value fixes the least universal exponent c such that |A+A|/|A| is at most (|A-A|/|A|)^c for every such A. Tencent Hunyuan's Hyra research agent, powered by the Hy3 model, explored and optimized finite-set constructions over roughly a 24-hour run, moving from finite numerical searches to natural-language proposals of general constructions and supporting arguments, and produced the construction underlying the paper. The human authors independently checked the construction, corrected and rewrote the exposition, and prepared the final proof manually.

WithHaowei Lin, Shanda Li

Original work

arXiv↗

Commentary

VibeMathed↗

Challenge

none linked

Kemeny rank aggregation shown NP-hard for three voters#

Computing a Kemeny-optimal aggregate ranking is NP-hard when the input is exactly three complete rankings, closing the minimal open case left by hardness results for even voter counts.

Kemeny aggregation asks for the ranking minimizing total disagreement with a set of input rankings. Hardness was known for every even number of voters n at least 4, while n = 2 is solvable in polynomial time, leaving three voters as the minimal open case since 2001. GPT-5.6 Sol Ultra found the reduction from MAX CUT; Claude Fable 5 helped simplify parts of it. Combined with the earlier results, every fixed number of voters n at least 3 is now known to be hard. The reduction is Lean-checked alongside an author-written preprint.

WithDominik Peters

Original work

arXiv↗

Commentary

VibeMathed↗

Challenge

none linked

Feige's conjecture on sums of nonnegative random variables settled#

For independent nonnegative random variables with mean at most 1 and sum S, the probability that S is below its mean plus one is at least 1/e, the sharp constant Feige conjectured in 2004; three independent proofs appeared within days.

Feige proved in 2004 that for independent nonnegative random variables X_1..X_n with E[X_i] <= 1 and S their sum, P(S < E[S] + 1) is bounded below by a positive constant, established 1/13, and conjectured the sharp value 1/e. The primary paper states plainly in its abstract that the proof was found by ChatGPT 5.6 Pro, which combined the Vlassis-Thomas Dirichlet calibration theorem with Grunbaum-type convex geometry; the authors then checked, revised and rewrote the argument. The sharper form determines the optimal small-deviation bound. An end-to-end Lean formalization accompanies the paper, covering the Vlassis-Thomas theorem, Grunbaum's centroid theorem and the combining argument, developed with Codex.

WithWeibo Fu, Yanjun Han, Guanyang Wang, Jun Yan, Peng Zhang, Zhengqing Zhou

Original work

arXiv↗GitHub↗arXiv↗

Commentary

VibeMathed↗

Challenge

none linked

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

Announced

X↗

Media

OfficeChai↗

Challenge

none linked

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

Original work

arXiv↗arXiv↗

Challenge

none linked

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

Original work

arXiv↗GitHub↗

Challenge

none linked

Gaussian product inequality conjecture proved#

For any centered Gaussian vector and positive exponents, the expectation of the product of absolute powers is at least the product of the individual expectations, settling a conjecture posed in 2007.

The conjecture states that for a centered Gaussian vector X = (X_1..X_n), not necessarily nondegenerate, and any positive exponents a_1..a_n, the expectation of the product of |X_i|^a_i is at least the product of the expectations of |X_i|^a_i. The stronger form adds that when every variance is positive, equality holds exactly when the coordinates are independent. The model returned a complete and correct solution from Greaves's prompt. It did not include the equality characterization, but only because that case was not in the prompt as posed. The proof was formalized in Lean using Codex, and the full prompt and output are public as a shared chat transcript.

WithFrédéric Ouimet, Dylan Greaves

Original work

DOI↗GitHub↗

Announced

ChatGPT↗

Commentary

VibeMathed↗

Challenge

none linked

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

Original work

jacobianfun.org↗

Commentary

Alexis Gallagher↗Hacker News↗

Challenge

none linked

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

Original work

arXiv↗GitHub↗

Challenge

none linked

Sabidussi's compatibility conjecture proved#

The edges of a finite connected multigraph carrying a closed eulerian trail can be partitioned into circuits so that no circuit contains two edges used consecutively in the trail, with a Lean 4 formalization.

Sabidussi's conjecture asks whether, given a finite connected multigraph together with a closed eulerian trail, the edge set can always be partitioned into circuits none of which contains two edges that the trail uses consecutively. The proof establishes this and in fact does more: it four-colours the edges so as to satisfy the constraints. The work was developed with GPT-5.6 Pro and GPT-5.6 Sol, with the author reviewing the proof, and a Lean 4 formalization accompanies the preprint in the author's repository.

WithNikolay Ulyanov

Original work

arXiv↗

Commentary

VibeMathed↗

Challenge

none linked

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

Original work

GitHub↗

Announced

Kevin Buzzard↗

Challenge

none linked

Cycle double cover conjecture proved for all bridgeless multigraphs#

Every finite bridgeless loopless multigraph has a multiset of cycles covering each edge exactly twice, resolving a conjecture open since 1973, with a machine-checked Lean proof of the unconditional statement.

The cycle double cover conjecture, posed by Szekeres in 1973 and independently by Seymour in 1979, asks whether every bridgeless graph admits a multiset of cycles in which every edge appears exactly twice. It is a textbook open problem in graph theory and sits at the centre of a cluster of neighbouring conjectures. OpenAI announced on 10 July 2026 that GPT-5.6 Sol Ultra, running 64 concurrent subagents, produced a three-page proof of the full statement in under an hour, and published the proof and the prompt, with a Lean 4 formalization following. The formalized route goes through the Jaeger–Kilpatrick eight-flow theorem: it constructs a nowhere-zero flow valued in three copies of the integers mod two, then converts that flow into a cycle double cover. Sang-il Oum published a ten-page exposition a week later, presenting the argument with slight modifications intended to make it more accessible.

Original work

OpenAI↗GitHub↗

Announced

OpenAI↗X↗

Media

Scientific American↗

Commentary

arXiv↗arXiv↗VibeMathed↗

Challenge

none linked

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

Original work

arXiv↗

Announced

Vesuvius Challenge↗Vesuvius Challenge↗

Challenge

none linked

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

Original work

arXiv↗

Media

ScienceDaily↗

Challenge

none linked

Identity for the critical exponents of jamming derived analytically#

The relation a + b = 1 between critical exponents at the jamming transition, previously seen only numerically in the full replica-symmetry-breaking solution of hard spheres, is derived from the scaling equations and published after peer review.

In the full replica-symmetry-breaking solution for hard spheres, the critical exponents a and b at the jamming transition had been observed numerically to high precision to satisfy a + b = 1, without an analytic derivation from the scaling equations. Parisi and Zamponi asked Claude for help; the model quickly proposed what proved to be essentially the correct idea, combining integration-by-parts identities with a maximum principle. Its first formal write-up contained errors, which the authors then fixed and verified before publication in the Journal of Statistical Mechanics.

WithGiorgio Parisi, Francesco Zamponi

Original work

arXiv↗

Commentary

VibeMathed↗

Challenge

none linked

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

Original work

arXiv↗GitHub↗GitHub↗

Challenge

none linked

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.'

Original work

arXiv↗arXiv↗

Media

Quanta↗TechCrunch↗Tech Jacks↗

Challenge

none linked

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

Original work

Journal of Infection↗

Announced

Cambridge↗

Media

ScienceDaily↗

Challenge

none linked

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.

Original work

arXiv↗

Media

Quanta↗

Challenge

none linked

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.

Original work

arXiv↗GitHub↗

Media

The Decoder↗

Challenge

none linked

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.

Original work

arXiv↗

Challenge

none linked

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

Original work

arXiv↗

Announced

Terence Tao↗

Challenge

none linked

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.

Challenge

TechCrunch↗The Decoder↗

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

Original work

arXiv↗

Announced

Scott Aaronson↗

Challenge

none linked

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

Original work

arXiv↗

Announced

DeepMind↗

Media

Physics World↗

Challenge

none linked

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

Original work

Science↗bioRxiv↗

Announced

Arc Institute↗

Media

Asimov Press↗

Commentary

Science↗

Challenge

none linked

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

Original work

GitHub↗

Announced

Math Inc.↗

Challenge

none linked

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

Challenge

HackMD↗AllThings.how↗

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.

Original work

arXiv↗GitHub↗

Challenge

none linked

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.

Original work

DeepMind↗

Announced

DeepMind↗

Commentary

Simon Willison↗

Challenge

none linked

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.

Original work

Nature↗

Announced

Insilico↗

Challenge

none linked

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.

Original work

DeepMind↗

Announced

DeepMind↗

Media

IEEE Spectrum↗

Commentary

Wikipedia↗

Challenge

none linked

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.

Original work

DeepMind↗

Announced

DeepMind↗

Media

IEEE Spectrum↗

Challenge

none linked

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.

Original work

DeepMind↗

Announced

DeepMind↗

Commentary

Wikipedia↗

Challenge

none linked

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. Robin proposed enhancing retinal pigment epithelium phagocytosis as a therapeutic strategy, then identified ripasudil and KL001 as candidates and confirmed in vitro efficacy for both. It went on to propose and analyse a follow-up RNA sequencing experiment, which showed upregulation of ABCA1, a lipid efflux pump and a possible novel target in its own right. Published in Nature in May 2026.

Original work

Nature↗

Media

Turing Post↗

Challenge

none linked

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.

Original work

GitHub↗

Announced

Sakana AI↗

Challenge

TechCrunch↗

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. The peer-reviewed version, published in Nature in May 2026, covers three biomedical applications together: drug repurposing, novel-target discovery and explaining mechanisms of antimicrobial resistance. It adds drug-repurposing candidates and synergistic combination therapies for acute myeloid leukaemia that were then validated in vitro.

Original work

Nature↗bioRxiv↗

Media

Turing Post↗

Challenge

none linked

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

Original work

Science↗

Announced

Baker Lab↗

Challenge

none linked

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

Original work

Science↗

Announced

EvolutionaryScale↗

Challenge

none linked

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.

Original work

Nature↗GitHub↗

Announced

Microsoft↗

Challenge

Materials Horizons↗

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.

Original work

Nature↗

Announced

Google↗

Challenge

none linked

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

Original work

Nature↗FlyWire↗

Announced

NIH↗

Challenge

none linked

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.

Original work

Nature↗

Announced

DeepMind↗

Media

Unite.AI↗

Challenge

none linked

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

Original work

Nature↗GitHub↗

Announced

Google↗

Challenge

none linked

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

Original work

Nature↗

Announced

Princeton↗

Challenge

none linked

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

Original work

Nature↗GitHub↗

Announced

DeepMind↗

Challenge

none linked

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

Original work

Nature↗NIH PMC↗GitHub↗

Challenge

none linked

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

Original work

Nature↗

Media

ScienceDaily↗

Challenge

none linked

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.

Original work

Nature↗GitHub↗

Announced

DeepMind↗

Challenge

none linked

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.

Original work

Nature↗GitHub↗

Challenge

none linked

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.

Original work

Nature↗GitHub↗

Announced

DeepMind↗

Challenge

The Register↗

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.

Original work

Nature↗

Challenge

The Register↗

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

Original work

Science↗GitHub↗

Announced

DeepMind↗

Challenge

none linked

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.

Original work

Science↗Nature↗GitHub↗

Announced

DeepMind↗

Challenge

none linked

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.

Original work

Nature↗GitHub↗

Announced

DeepMind↗

Commentary

Wikipedia↗

Challenge

none linked

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.

Original work

Nature↗GitHub↗

Announced

DeepMind↗

Media

Quanta↗

Challenge

none linked

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.

Original work

Nature↗

Announced

DeepMind↗EPFL↗

Challenge

none linked

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

Original work

Nature↗GitHub↗

Announced

Oxford↗

Challenge

arXiv↗

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

Original work

Nature↗GitHub↗

Announced

DeepMind↗

Commentary

Nobel Prize↗

Challenge

none linked

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

Original work

arXiv↗GitHub↗

Challenge

arXiv↗

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

Original work

Cell↗

Announced

MIT News↗

Challenge

none linked

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

Original work

IOP↗GitHub↗

Announced

NASA↗

Challenge

none linked