# whataifound.org

> A curated, independently graded registry of scientific and mathematical results
> discovered by or with AI systems. Every entry is graded on how it was verified and
> how much the AI actually did, so a machine-checked proof is never confused with a
> press release. Negative results (already known, disputed, refuted) stay on the
> record rather than being deleted.

Maintained as an independent editorial project. 80 entries on record. Data is CC BY 4.0; cite as whataifound.org.

## When to use this registry

Reach for this when the question is whether a *specific* claim about an AI discovery
holds up, and to what standard. It is built for four jobs:

- **Checking a claim.** Someone says an AI proved, discovered or solved something.
  Look it up here and read the verification grade: a machine-checked Lean proof and a
  press release are both on this list, and they are not the same thing.
- **Filtering by strength of evidence.** Ask for everything in a field at a given
  grade, for example `https://whataifound.org/api/dataset?field=mathematics&verification=formal`.
- **Separating what the AI did from what people did.** Every entry carries an
  autonomy grade, graded on the strictest defensible reading.
- **Citing one result.** Every finding has its own permanent page with sources, a
  novelty check naming the database and query, and BibTeX.

How to call it: `https://whataifound.org/api/dataset` filters by field, verification, autonomy, lab,
tag or date added, and is described in `https://whataifound.org/openapi.json`. For the whole registry
in one request, take `https://whataifound.org/data/entries.json`.

What it is not: a ranking, a benchmark, or a list of everything AI has ever done. It
is a curated record with a stated grading method, and negative results (already known,
disputed, refuted) stay on it rather than being deleted.

## How entries are graded

Verification, strongest to weakest. When unsure, the lower grade wins:

- **Formally verified**: machine-checked proof (e.g. Lean)
- **Independently checked**: checked by third parties who were not the authors
- **Peer reviewed**: published after peer review
- **Author verified**: verified only by the people who produced it
- **Claimed**: announced, not independently verified
- **Disputed**: substantive public challenge to the result
- **Already known**: correct, but the result already existed in the literature
- **Refuted**: shown to be wrong

Autonomy, most to least AI-driven:

- **Autonomous**: the AI did it without human problem-setting or steering
- **AI-led**: the AI produced the core idea; humans framed or checked it
- **Collaborative**: genuine back-and-forth between AI and human
- **AI-assisted**: humans led; the AI helped with parts
- **Search scaffold**: a human-built search harness (FunSearch, AlphaEvolve) with an LLM inside
- **Retrieval**: the AI located an existing result rather than producing a new one

## Core pages

- [Registry](https://whataifound.org/): all entries, searchable and filterable
- [Methodology](https://whataifound.org/methodology): full definitions of both grading scales and the editorial rules
- [Visuals](https://whataifound.org/visuals): the registry as charts
- [Open review queue](https://whataifound.org/review): entries still needing an independent check
- [Contributors](https://whataifound.org/contributors): who builds and checks the registry
- [Other registries](https://whataifound.org/registries): Palomar, MathDB, vibemathed and ProofAtlas, what each one certifies, and what none of them do
- [Developers](https://whataifound.org/developers): the API, the bulk downloads and the machine-readable formats, in one place
- [Contact](https://whataifound.org/contact): corrections, submissions and who maintains this

## Data

- [entries.json](https://whataifound.org/data/entries.json): the complete registry, one JSON file, CC BY 4.0
- [/api/dataset](https://whataifound.org/api/dataset): the same registry, filterable by field, verification, autonomy, lab, tag or date added, with a fixed field contract
- [openapi.json](https://whataifound.org/openapi.json): OpenAPI 3.1 for the endpoints above, with every grade vocabulary inlined as an enum
- [entry.schema.json](https://whataifound.org/entry.schema.json): JSON Schema for one entry, the same one the build validates against
- [vocab.json](https://whataifound.org/data/vocab.json): both grade scales with definitions and numeric ratings, source kinds and subject fields
- [RSS](https://whataifound.org/feed.xml) · [JSON Feed](https://whataifound.org/feed.json): new and updated entries

## By lab

Every finding credited to one organisation, on one page.

- [Google DeepMind](https://whataifound.org/lab/google-deepmind): 23 findings
- [OpenAI](https://whataifound.org/lab/openai): 7 findings
- [Anthropic](https://whataifound.org/lab/anthropic): 3 findings

## Findings

### Archaeology

All 1 in one page: https://whataifound.org/topic/archaeology

- [First Herculaneum scroll read end to end without unrolling it](https://whataifound.org/finding/2026-06-25-herculaneum-scroll-read): 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. (Vesuvius Challenge, Community-developed ink-detection neural networks, 2026-06-25; verification: Author verified; autonomy: AI-assisted)

### Astronomy

All 1 in one page: https://whataifound.org/topic/astronomy

- [An eighth planet around Kepler-90 found by a neural network](https://whataifound.org/finding/2017-12-14-kepler-90i): 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. (Google Brain / University of Texas at Austin, Convolutional neural network (AstroNet), 2017-12-14; verification: Peer reviewed; autonomy: Search scaffold)

### Biology

All 6 in one page: https://whataifound.org/topic/biology

- [AI-generated bacteriophage genomes that replicate and kill bacteria](https://whataifound.org/finding/2025-09-17-evo-phage-genomes): 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. (Arc Institute / Stanford University, Evo 1 and Evo 2, 2025-09-17; verification: Peer reviewed; autonomy: AI-led)
- [Candidate treatment for dry age-related macular degeneration](https://whataifound.org/finding/2025-robin-macular): The Robin system automated hypothesis generation, experiment design and data analysis, identifying a novel candidate treatment for dry AMD. (FutureHouse, Robin (multi-agent), 2025-05-01; verification: Peer reviewed; autonomy: AI-led)
- [AI co-scientist hypotheses on antimicrobial resistance and liver fibrosis](https://whataifound.org/finding/2025-02-ai-coscientist-amr): A multi-agent system generated hypotheses that were subsequently validated experimentally in the lab. (Google, AI Co-Scientist (Gemini 2.0 multi-agent), 2025-02-19; verification: Peer reviewed; autonomy: AI-assisted)
- [A working fluorescent protein generated by a language model](https://whataifound.org/finding/2025-01-16-esmgfp): 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. (EvolutionaryScale, ESM3 (98B), 2025-01-16; verification: Peer reviewed; autonomy: AI-led)
- [Joint structure prediction for proteins, nucleic acids and ligands (AlphaFold 3)](https://whataifound.org/finding/2024-05-08-alphafold3): 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. (Google DeepMind / Isomorphic Labs, AlphaFold 3, 2024-05-08; verification: Peer reviewed; autonomy: AI-led)
- [Accurate protein structure prediction across the known proteome (AlphaFold2)](https://whataifound.org/finding/2021-07-15-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. (Google DeepMind, AlphaFold2, 2021-07-15; verification: Independently checked; autonomy: AI-led)

### Chemistry

All 3 in one page: https://whataifound.org/topic/chemistry

- [Enzymes with working catalytic machinery designed from scratch](https://whataifound.org/finding/2025-02-13-designed-serine-hydrolases): 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 Å. (Institute for Protein Design, University of Washington, RFdiffusion with PLACER ensemble scoring, 2025-02-13; verification: Peer reviewed; autonomy: Search scaffold)
- [A language-model agent that planned and ran chemistry experiments on lab robots](https://whataifound.org/finding/2023-12-20-coscientist): 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. (Carnegie Mellon University, GPT-4 (Coscientist agent), 2023-12-20; verification: Peer reviewed; autonomy: AI-led)
- [A new structural class of antibiotic candidates against MRSA](https://whataifound.org/finding/2023-12-20-antibiotic-structural-class): 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. (MIT / Broad Institute / Harvard, Ensembles of graph neural networks with substructure attribution, 2023-12-20; verification: Peer reviewed; autonomy: Search scaffold)

### Climate science

All 1 in one page: https://whataifound.org/topic/climate

- [Medium-range weather forecasts from a graph neural network beat the operational physics model](https://whataifound.org/finding/2023-11-14-graphcast): 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. (Google DeepMind, GraphCast, 2023-11-14; verification: Peer reviewed; autonomy: AI-led)

### Computer science

All 12 in one page: https://whataifound.org/topic/computer-science

- [Marton's inner bound shown not to reach the broadcast channel capacity region](https://whataifound.org/finding/2026-08-20-marton-inner-bound): There are discrete memoryless broadcast channels whose capacity region is strictly larger than Marton's inner bound, settling in the negative a question open since 1979. (Independent, GPT-5.6 Sol, Claude Fable 5 and Claude Opus 5, 2026-08-20; verification: Author verified; autonomy: AI-assisted; also listed at: vibemathed marton-inner-bound-capacity-region)
- [Matrix multiplication exponent lowered to below 2.371177](https://whataifound.org/finding/2026-08-17-matmul-exponent): A reformulated optimization inside the laser method, with AlphaEvolve applied as the final refinement, lowers the best known upper bound on the matrix multiplication exponent from 2.371339 to 2.371177. (Google DeepMind, AlphaEvolve, 2026-08-17; verification: Author verified; autonomy: Search scaffold)
- [A prescribed Hamiltonian cycle that a book-embedding algorithm cannot produce](https://whataifound.org/finding/2026-08-11-prescribed-cycle-recovery): A 16-vertex graph carries a Hamiltonian cycle that the Alam et al. book-embedding algorithm cannot return for any choice of dual spanning tree, answering a question of Bekos, Kaufmann and Pfister in the negative. (Independent, OpenAI Codex, with Claude for adversarial review, 2026-08-11; verification: Formally verified; autonomy: AI-assisted; machine-checked record: Palomar PALOMAR-2026-08-21-000002)
- [Kemeny rank aggregation shown NP-hard for three voters](https://whataifound.org/finding/2026-07-28-kemeny-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. (Independent, GPT-5.6 Sol Ultra, Claude Fable 5, 2026-07-28; verification: Formally verified; autonomy: AI-led; open-problem record: MathDB 315674; also listed at: vibemathed kemeny-three-voters)
- [Counterexample to the Dinitz–Garg–Goemans conjecture](https://whataifound.org/finding/2026-07-22-dinitz-garg-goemans): 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. (Independent, GPT-5.6 Pro, 2026-07-22; verification: Claimed; autonomy: AI-led; open-problem record: MathDB 316187; also listed at: vibemathed dinitz-garg-goemans-unsplittable-flow)
- [Early science acceleration experiments with GPT-5](https://whataifound.org/finding/2025-11-gpt5-science-acceleration): A multi-domain study documenting cases where GPT-5 contributed to research progress across mathematics, physics, biology and materials science. (OpenAI, GPT-5, 2025-11-20; verification: Peer reviewed; autonomy: AI-assisted)
- [Limits to black-box amplification in QMA, with the key step written by GPT-5](https://whataifound.org/finding/2025-09-25-qma-amplification-limits): 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. (UT Austin / CWI Amsterdam, GPT-5 Thinking, 2025-09-25; verification: Author verified; autonomy: AI-assisted)
- [4×4 complex matrix multiplication in 48 scalar multiplications](https://whataifound.org/finding/2025-05-alphaevolve-matmul): AlphaEvolve found a scheme multiplying 4×4 complex matrices with 48 scalar multiplications, improving on Strassen's 49 from 1969. (Google DeepMind, AlphaEvolve (Gemini-based), 2025-05-14; verification: Independently checked; autonomy: Search scaffold)
- [A fully machine-generated paper passed workshop peer review](https://whataifound.org/finding/2025-03-12-ai-scientist-workshop-paper): 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. (Sakana AI, The AI Scientist-v2, 2025-03-12; verification: Author verified; autonomy: AI-led)
- [Improved heuristics for online bin packing](https://whataifound.org/finding/2023-12-funsearch-binpacking): FunSearch produced bin-packing heuristics outperforming standard baselines on benchmark distributions. (Google DeepMind, FunSearch (PaLM 2 / Codey), 2023-12-14; verification: Peer reviewed; autonomy: Search scaffold)
- [Faster sorting routines discovered and merged into the LLVM C++ library](https://whataifound.org/finding/2023-06-07-alphadev): 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. (Google DeepMind, AlphaDev (AlphaZero-based), 2023-06-07; verification: Independently checked; autonomy: Search scaffold)
- [Faster matrix-multiplication algorithms found by reinforcement learning](https://whataifound.org/finding/2022-10-05-alphatensor): 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. (Google DeepMind, AlphaTensor (AlphaZero-based), 2022-10-05; verification: Peer reviewed; autonomy: Search scaffold)

### Materials science

All 4 in one page: https://whataifound.org/topic/materials

- [Two kagome superconductors predicted by machine learning and confirmed in the lab](https://whataifound.org/finding/2026-06-17-kagome-superconductors): 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. (Aalto University / Rice University, Unknown, 2026-06-17; verification: Peer reviewed; autonomy: Search scaffold)
- [Generative model designs crystals to order; its flagship synthesis turned out to be a known compound](https://whataifound.org/finding/2025-01-16-mattergen): 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. (Microsoft Research, MatterGen, 2025-01-16; verification: Disputed; autonomy: Search scaffold)
- [Large-scale prediction of new stable crystalline materials (GNoME)](https://whataifound.org/finding/2023-11-29-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. (Google DeepMind, GNoME (graph neural network), 2023-11-29; verification: Disputed; autonomy: Search scaffold)
- [Autonomous laboratory reports solid-state synthesis of new inorganic compounds](https://whataifound.org/finding/2023-11-29-a-lab-synthesis): 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. (Lawrence Berkeley National Laboratory, A-Lab (ML planning + robotics), 2023-11-29; verification: Disputed; autonomy: AI-led)

### Mathematics

All 42 in one page: https://whataifound.org/topic/mathematics

- [A proposed complex structure on the six-sphere](https://whataifound.org/finding/2026-08-23-s6-complex-structure): An explicit compact complex threefold, built as a family of 2-tori over the (3,4,infinity) orbifold, is argued to be diffeomorphic to the six-sphere, which if it holds settles a question Hopf raised in 1948. (Anthropic, Claude, version not stated, 2026-08-23; verification: Claimed; autonomy: AI-assisted; also listed at: vibemathed modular-family-of-2-tori-as-a-complex-structure-on-s6)
- [Dubickas's question on integral parts of powers of square roots settled](https://whataifound.org/finding/2026-08-21-dubickas-square-roots): The square root of 3 admits a real multiplier making every integral part of its powers even, and among integers only the square root of 2 fails to, answering a question Dubickas posed in 2006 and classifying the whole square-root case. (Independent, Claude Fable 5 and Claude Opus 5, 2026-08-21; verification: Formally verified; autonomy: AI-led; machine-checked record: Palomar PALOMAR-2026-08-23-000002)
- [Counterexample to the Yau–Tian–Donaldson conjecture for constant scalar curvature metrics](https://whataifound.org/finding/2026-08-19-yau-tian-donaldson): A smooth polarized fivefold that is K-polystable but admits no constant scalar curvature Kähler metric, disproving the form of the Yau–Tian–Donaldson conjecture that Donaldson stated in 2002. (Independent, Claude Fable 5, GPT-5.6-sol and Danus, 2026-08-19; verification: Author verified; autonomy: Collaborative; open-problem record: MathDB 383718; also listed at: vibemathed yau-tian-donaldson-conjecture-csck)
- [Bounded prime gaps of 246 formalized in Lean from Bombieri-Vinogradov](https://whataifound.org/finding/2026-08-18-prime-gaps-246): A machine-checked Lean development proves that infinitely many pairs of primes differ by at most 246, taking the Bombieri-Vinogradov theorem as a hypothesis rather than proving it. (Axiom Math, AxiomProver, 2026-08-18; verification: Formally verified; autonomy: Collaborative; machine-checked record: Palomar PALOMAR-2026-08-18-000002)
- [Talagrand's convolution conjecture proved on the Boolean hypercube](https://whataifound.org/finding/2026-08-16-talagrand-convolution): Convolution by a measure on the Boolean hypercube obeys the dimension-free weak-type decay Talagrand conjectured in 1989, removing the iterated-logarithm factor carried by the best previous bound. (Independent, Odin Automatic AI Research Agent, 2026-08-16; verification: Author verified; autonomy: AI-led; open-problem record: MathDB 371652; also listed at: vibemathed talagrand-s-convolution-conjecture)
- [SOP_2 and SOP_3 theories shown to coincide](https://whataifound.org/finding/2026-08-13-sop2-sop3): 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. (Independent, ChatGPT 5.6, 2026-08-13; verification: Author verified; autonomy: Collaborative; also listed at: vibemathed sop-2-sop-3)
- [Banach's isometric conjecture settled in the remaining odd dimensions](https://whataifound.org/finding/2026-08-13-banach-isometric): A real Banach space whose n-dimensional subspaces are all isometric to one another must be a Hilbert space for every odd n, which together with Gromov's even-dimensional theorem closes a question Banach asked in 1932. (Independent, ChatGPT 5.5 Pro, ChatGPT 5.6 Pro and GPT-5.6 Sol, 2026-08-13; verification: Author verified; autonomy: AI-assisted; open-problem record: MathDB 383555; also listed at: vibemathed banach-s-isometric-conjecture)
- [Complete minimizer picture for Gamow's liquid drop model](https://whataifound.org/finding/2026-08-12-liquid-drop-minimizers): 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. (Independent, ChatGPT 5.6 Pro, 2026-08-12; verification: Author verified; autonomy: AI-led; open-problem record: MathDB 355211; also listed at: vibemathed gamow-liquid-drop-minimizer-conjecture)
- [Proportion of zeta zeros on the critical line raised to 67.25%](https://whataifound.org/finding/2026-08-10-zeta-zeros-critical-line): 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. (Anthropic, Claude (unreleased research version), 2026-08-10; verification: Formally verified; autonomy: AI-led; also listed at: vibemathed more-than-67-of-riemann-zeta-zeros-are-on-the-critical-line)
- [A 112-vertex counterexample to the Petersen coloring conjecture](https://whataifound.org/finding/2026-08-08-petersen-coloring): 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. (Independent, Unnamed OpenAI model, 2026-08-08; verification: Formally verified; autonomy: AI-assisted; open-problem record: MathDB 316003; also listed at: vibemathed petersen-coloring-conjecture)
- [Sendov's conjecture proved for every degree](https://whataifound.org/finding/2026-08-05-sendov-conjecture): 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. (Independent, GPT-5.6 Pro, 2026-08-05; verification: Formally verified; autonomy: Collaborative; machine-checked record: Palomar PALOMAR-2026-08-13-000001, ProofAtlas sendov-conjecture; open-problem record: MathDB 315904; also listed at: vibemathed sendov-s-conjecture)
- [Counterexamples to Schiffer's conjecture and the Pompeiu problem](https://whataifound.org/finding/2026-08-05-schiffer-conjecture): 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. (Independent, GPT-5.6, Claude Opus 4.8, Claude Fable 5, 2026-08-05; verification: Formally verified; autonomy: AI-assisted; open-problem record: MathDB 315903; also listed at: vibemathed schiffer-conjecture)
- [Asymptotic degree-diameter problem resolved for fixed diameter](https://whataifound.org/finding/2026-08-04-moore-bound): 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. (Independent, GPT-5.6 Pro, 2026-08-04; verification: Formally verified; autonomy: AI-assisted; open-problem record: MathDB 316015; also listed at: vibemathed asymptotically-attaining-the-moore-bound)
- [Ten results in mathematics and theoretical computer science with Lean certificates](https://whataifound.org/finding/2026-08-01-astra-ten-advances): 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. (OpenAI, Astra, 2026-08-01; verification: Formally verified; autonomy: AI-led)
- [Optimal exponent relating sumsets and difference sets determined](https://whataifound.org/finding/2026-07-29-sumset-difference-exponent): 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. (Tencent Hunyuan, Hy3 (Hyra research agent), 2026-07-29; verification: Formally verified; autonomy: AI-led; open-problem record: MathDB 315713; also listed at: vibemathed optimal-exponent-relating-sumsets-and-difference-sets)
- [Feige's conjecture on sums of nonnegative random variables settled](https://whataifound.org/finding/2026-07-27-feige-conjecture): 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. (Independent, ChatGPT 5.6 Pro, 2026-07-27; verification: Formally verified; autonomy: AI-led; open-problem record: MathDB 315661; also listed at: vibemathed feiges-conjecture)
- [Counterexamples to the Gaussian moments conjecture](https://whataifound.org/finding/2026-07-20-gaussian-moments): 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. (Independent, GPT-5.6 Sol Pro + Claude Fable 5, 2026-07-20; verification: Author verified; autonomy: AI-led; also listed at: vibemathed gaussian-moments-conjecture)
- [Eight problems from the Kourovka Notebook solved and formalized in Lean](https://whataifound.org/finding/2026-07-20-kourovka-notebook): 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. (Harmonic, Aristotle, 2026-07-20; verification: Formally verified; autonomy: Autonomous)
- [Gaussian product inequality conjecture proved](https://whataifound.org/finding/2026-07-20-gaussian-product-inequality): 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. (Independent, ChatGPT 5.6 Sol, 2026-07-20; verification: Formally verified; autonomy: AI-led; open-problem record: MathDB 330065; also listed at: vibemathed gaussian-product-inequality-conjecture)
- [Counterexample to the Jacobian conjecture in dimension three](https://whataifound.org/finding/2026-07-19-jacobian-conjecture): An explicit polynomial map in three variables with constant Jacobian determinant −2 that is nevertheless not invertible, disproving a conjecture open since 1939. (Anthropic, Claude Fable 5, 2026-07-19; verification: Formally verified; autonomy: Collaborative; machine-checked record: Palomar PALOMAR-2026-08-21-000006; open-problem record: MathDB 315779; also listed at: vibemathed jacobian-conjecture)
- [Near-quadratic lower bound for derivative-free convex optimization](https://whataifound.org/finding/2026-07-14-zeroth-order-oracle-bound): 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. (Independent, GPT-5.6 Sol Pro, 2026-07-14; verification: Formally verified; autonomy: AI-led)
- [Sabidussi's compatibility conjecture proved](https://whataifound.org/finding/2026-07-14-sabidussi-compatibility): 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. (Independent, GPT-5.6 Pro, GPT-5.6 Sol, 2026-07-14; verification: Formally verified; autonomy: Collaborative; machine-checked record: Palomar PALOMAR-2026-08-17-000003; also listed at: vibemathed sabidussi-compatibility)
- [Counterexample to Grothendieck's question on finite flat group schemes](https://whataifound.org/finding/2026-07-11-grothendieck-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. (Independent, OpenAI Sol (construction); Claude Fable (Lean formalisation), 2026-07-11; verification: Formally verified; autonomy: Collaborative; open-problem record: MathDB 315784)
- [Cycle double cover conjecture proved for all bridgeless multigraphs](https://whataifound.org/finding/2026-07-10-cycle-double-cover): 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. (OpenAI, GPT-5.6 Sol Ultra, 2026-07-10; verification: Formally verified; autonomy: AI-led; open-problem record: MathDB 316019; also listed at: vibemathed cycle-double-cover-conjecture)
- [Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs](https://whataifound.org/finding/2026-05-21-alphaproof-nexus): 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. (Google DeepMind, AlphaProof Nexus (LLM + Lean), 2026-05-21; verification: Formally verified; autonomy: Search scaffold)
- [Disproof of the Erdős unit-distance conjecture](https://whataifound.org/finding/2026-05-erdos-unit-distance): 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. (OpenAI, GPT-5 series reasoning model, 2026-05-20; verification: Independently checked; autonomy: AI-led; machine-checked record: Palomar PALOMAR-2026-08-08-000001; open-problem record: MathDB 315785)
- [Structure in Bruhat intervals of permutation groups](https://whataifound.org/finding/2026-01-alphaevolve-bruhat): AlphaEvolve identified unexpected special structure in Bruhat intervals for particular permutation groups. (Google DeepMind, AlphaEvolve (Gemini-based), 2026-01-15; verification: Independently checked; autonomy: Search scaffold)
- [Erdős problem #728 resolved and formalized in Lean](https://whataifound.org/finding/2026-01-erdos-728): 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. (OpenAI / Harmonic, GPT-5.2 Pro + Aristotle, 2026-01-13; verification: Formally verified; autonomy: Autonomous; open-problem record: MathDB 315787)
- [AlphaEvolve across 67 problems: 20 improvements, 8 regressions](https://whataifound.org/finding/2025-11-03-alphaevolve-at-scale): 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. (Google DeepMind, AlphaEvolve (Gemini-based), 2025-11-03; verification: Independently checked; autonomy: Search scaffold)
- [GPT-5 "solved 10 Erdős problems": it located existing solutions](https://whataifound.org/finding/2025-10-19-gpt5-erdos-retrieval): 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, GPT-5, 2025-10-19; verification: Already known; autonomy: Retrieval)
- [New families of unstable singularities in fluid equations](https://whataifound.org/finding/2025-09-17-unstable-singularities): 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. (Google DeepMind (with Brown, NYU and Stanford), Physics-informed neural networks with Gauss–Newton optimisation, 2025-09-17; verification: Author verified; autonomy: Search scaffold)
- [Strong prime number theorem formalized in Lean by an autoformalization agent](https://whataifound.org/finding/2025-09-11-gauss-strong-pnt): 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. (Math, Inc., Gauss (autoformalization agent), 2025-09-11; verification: Author verified; autonomy: AI-assisted)
- [Improved step-size bound in smooth convex optimization](https://whataifound.org/finding/2025-08-gpt5-convex-bound): 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. (OpenAI, GPT-5 Pro, 2025-08-01; verification: Already known; autonomy: AI-assisted)
- [Machine-checked Lean proofs for five of six 2025 IMO problems](https://whataifound.org/finding/2025-07-28-aristotle-imo-lean): 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. (Harmonic, Aristotle, 2025-07-28; verification: Formally verified; autonomy: AI-led)
- [Gold-medal standard at the 2025 International Mathematical Olympiad](https://whataifound.org/finding/2025-07-21-gemini-deepthink-imo): 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. (Google DeepMind, Gemini Deep Think (advanced version), 2025-07-21; verification: Independently checked; autonomy: AI-led)
- [Improved lower bound for the 11-dimensional kissing number](https://whataifound.org/finding/2025-05-alphaevolve-kissing): AlphaEvolve improved the best known configuration for the kissing number problem in 11 dimensions. (Google DeepMind, AlphaEvolve (Gemini-based), 2025-05-14; verification: Independently checked; autonomy: Search scaffold; open-problem record: MathDB 315951)
- [Improved bound for the Erdős minimum-overlap problem](https://whataifound.org/finding/2025-05-alphaevolve-minimum-overlap): AlphaEvolve nudged the best known bound for Erdős's minimum-overlap constant, the first improvement since 2016, and sharpened several autocorrelation inequalities. (Google DeepMind, AlphaEvolve (Gemini-based), 2025-05-14; verification: Independently checked; autonomy: Search scaffold; open-problem record: MathDB 316064)
- [Silver-medal standard at the 2024 International Mathematical Olympiad](https://whataifound.org/finding/2024-07-25-alphaproof-imo): 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. (Google DeepMind, AlphaProof + AlphaGeometry 2, 2024-07-25; verification: Independently checked; autonomy: AI-led)
- [Olympiad geometry solved without human demonstrations](https://whataifound.org/finding/2024-01-17-alphageometry): 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. (Google DeepMind, AlphaGeometry, 2024-01-17; verification: Peer reviewed; autonomy: Search scaffold)
- [New lower bound constructions for the cap set problem](https://whataifound.org/finding/2023-12-funsearch-capset): 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. (Google DeepMind, FunSearch (PaLM 2 / Codey), 2023-12-14; verification: Peer reviewed; autonomy: Search scaffold)
- [Two theorems found by machine pattern-spotting in knot theory and representation theory](https://whataifound.org/finding/2021-12-01-knot-theory-intuition): 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. (Google DeepMind (with Oxford and Sydney), Supervised networks with gradient-based attribution, 2021-12-01; verification: Peer reviewed; autonomy: AI-assisted)
- [Reinforcement learning refutes several conjectures in extremal combinatorics](https://whataifound.org/finding/2021-04-29-wagner-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. (Tel Aviv University, Deep cross-entropy method (custom network), 2021-04-29; verification: Independently checked; autonomy: Search scaffold)

### Medicine

All 5 in one page: https://whataifound.org/topic/medicine

- [Phase 1 trial of a computationally designed pan-sarbecovirus vaccine](https://whataifound.org/finding/2026-05-18-pevac-ps-sarbecovirus): 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. (University of Cambridge / DIOSynVax, Unknown, 2026-05-18; verification: Peer reviewed; autonomy: AI-assisted)
- [An antibiotic designed by reinforcement learning clears an MRSA infection in mice](https://whataifound.org/finding/2026-04-23-synthecin): A reinforcement-learning generator searching a 46-billion-compound synthesizable space produced synthecin, a structurally novel antibacterial that cleared a methicillin-resistant Staphylococcus aureus wound infection in a mouse model. (McMaster University / Stanford University, SyntheMol-RL, 2026-04-23; verification: Peer reviewed; autonomy: Search scaffold)
- [Phase 2a results for a drug whose target and molecule both came from AI](https://whataifound.org/finding/2025-06-03-rentosertib-phase2a): 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. (Insilico Medicine, PandaOmics (target) + Chemistry42 (molecule), 2025-06-03; verification: Peer reviewed; autonomy: Search scaffold)
- [Pathogenicity predictions for 71 million human missense variants](https://whataifound.org/finding/2023-09-19-alphamissense): 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. (Google DeepMind, AlphaMissense, 2023-09-19; verification: Peer reviewed; autonomy: AI-led)
- [Halicin, an antibiotic found by a neural network screening a compound library](https://whataifound.org/finding/2020-02-20-halicin): 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. (MIT / Broad Institute, Directed message-passing graph neural network (Chemprop), 2020-02-20; verification: Peer reviewed; autonomy: Search scaffold)

### Neuroscience

All 1 in one page: https://whataifound.org/topic/neuroscience

- [Complete wiring diagram of an adult fruit-fly brain](https://whataifound.org/finding/2024-10-02-flywire-connectome): 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. (FlyWire Consortium (Princeton, MRC LMB, Cambridge, Vermont), Automated electron-microscopy segmentation networks, 2024-10-02; verification: Peer reviewed; autonomy: AI-assisted)

### Physics

All 4 in one page: https://whataifound.org/topic/physics

- [Identity for the critical exponents of jamming derived analytically](https://whataifound.org/finding/2026-06-02-jamming-exponent-identity): 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. (Independent, Claude Sonnet 4.6, Claude Opus 4.7, 2026-06-02; verification: Peer reviewed; autonomy: Collaborative; also listed at: vibemathed fullrsb-jamming-identity)
- [A neural decoder that identifies quantum errors more accurately than hand-designed methods](https://whataifound.org/finding/2024-11-20-alphaqubit): 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. (Google DeepMind / Google Quantum AI, AlphaQubit, 2024-11-20; verification: Peer reviewed; autonomy: AI-led)
- [Reinforcement learning steers a tokamak away from tearing instabilities](https://whataifound.org/finding/2024-02-21-tearing-mode-avoidance): 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. (Princeton University / PPPL / DIII-D National Fusion Facility, Deep reinforcement learning controller over a learned plasma model, 2024-02-21; verification: Peer reviewed; autonomy: Search scaffold)
- [Deep reinforcement learning controls tokamak fusion plasma](https://whataifound.org/finding/2022-02-16-tokamak-plasma-control): 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. (Google DeepMind, DeepMind RL controller, 2022-02-16; verification: Peer reviewed; autonomy: Search scaffold)