whataifound.org Sign in

AI findings in mathematics

Every finding in the registry filed under mathematics, with what each one claims and how solid the evidence is.

By verification grade

17 of 82 carry an independent check. Open the review queue.

Open longest before falling

  1. 389 yrFermat's Last Theorem formalized end to end in Lean 4posed 1637 · Internal Anthropic research model, described in the announcement as roughly comparable to Claude Fable 5.1
  2. 331 yrImproved lower bound for the 11-dimensional kissing numberposed 1694 · AlphaEvolve (Gemini-based)
  3. 177 yrBounded prime gaps improved to 212, with a Lean certificate of the deductionposed 1849 · AxiomProver
  4. 177 yrPrime gaps at most 186, conditional on three unproved Lean axiomsposed 1849 · GPT-6 Astra

From the 53 of 82 entries recording a posed year. Add a missing one.

All findings in the registry, sortable by column.
DateFindingLabModelVerificationAutonomyField
2026-09-14 Nivat's conjecture claimed in its sharp form, with the submitter stating he cannot check it Independent GPT-6 Pro (proof); GPT-6 Astra Ultra through Codex (Lean formalization) Claimed AI-led mathematics
2026-09-08 Finite-time blowup for Navier-Stokes with smooth forcing, Clay alternatives C and D OpenAI Unnamed OpenAI model described as more capable than GPT-6 Astra for the proof; GPT-6 Astra through Codex for the Lean formalization Claimed AI-led mathematics
2026-09-08 Finite-time blowup for the unforced Euler equations from smooth compactly supported data OpenAI Unnamed OpenAI model described as more capable than GPT-6 Astra for the proof; GPT-6 Astra through Codex for the Lean formalization Claimed AI-led mathematics
2026-09-06 Bollobas-Nikiforov conjecture claimed in full, in a weighted form Independent GPT-6 Astra (ideation and manuscript); Grok 4.6 (Lean formalization); Claude Fable 5.1 (submission packaging) Claimed Collaborative mathematics
2026-09-05 Disproof of the Ibragimov-Iosifescu conjecture for phi-mixing sequences OpenAI / Epoch AI GPT-6 Astra (pre-release) Claimed AI-led mathematics
2026-09-04 Fermat's Last Theorem formalized end to end in Lean 4 Anthropic Internal Anthropic research model, described in the announcement as roughly comparable to Claude Fable 5.1 Formally verified AI-led mathematics
2026-09-03 Lean disproof of Krempa's matrix form of the Koethe conjecture OpenAI / Epoch AI GPT-6 Astra (pre-release) Formally verified Autonomous mathematics
2026-09-03 Erdos-Sos conjecture proved in Lean, in a form marginally weaker than the classical statement OpenAI / Epoch AI GPT-6 Astra (pre-release) Formally verified Autonomous mathematics
2026-09-03 Disputed claim that Catalan's constant is irrational Nanjing University ChatGPT 5.6 Solar, named in the paper as the verifier; the model consulted during the work is named only as AI Disputed AI-assisted mathematics
2026-09-03 Counterexample to Smale's mean value conjecture at K = 1 OpenAI / Epoch AI GPT-6 Astra (pre-release) Claimed Autonomous mathematics
2026-09-03 Bounded prime gaps improved to 212, with a Lean certificate of the deduction Axiom Math AxiomProver Claimed Collaborative mathematics
2026-09-02 Confirmation of the Daykin-Frankl conjecture from a language-model proof Independent GPT-5.6 Sol Pro Author verified AI-led mathematics
2026-09-02 A smooth counterexample to the Trautman conjecture Oklahoma State University ChatGPT Plus, version not named Author verified AI-assisted mathematics
2026-09-02 Prime gaps at most 186, conditional on three unproved Lean axioms OpenAI GPT-6 Astra Claimed AI-led mathematics
2026-09-01 Entropy production of the Boltzmann equation is not always monotone Independent GPT-5.6 Sol; Claude Author verified AI-led mathematics
2026-09-01 Common neighbour conjectures for Saxl graphs fail at every base size Independent Codex; ChatGPT Pro; Claude Formally verified Collaborative mathematics
2026-08-31 Counterexample to the stable forking conjecture Independent GPT-5.6 Sol Author verified Collaborative mathematics
2026-08-31 Criteria and two quadratic instances for Bugeaud's Problem 10.61 Independent Claude Fable 5; Claude Opus 5 Claimed AI-led mathematics
2026-08-29 Dean's conjecture for k = 5, cycles of length divisible by five Independent GPT-5.6 Sol; Claude Opus 5; GLM 5.3 Flash Claimed AI-led mathematics
2026-08-28 Lean proof that the percolation probability vanishes at the critical point in every dimension Anthropic Anthropic Claude models, versions not stated Claimed AI-led mathematics
2026-08-27 Hyperbolic surfaces with large systoles in every large genus Independent GPT-5.6 Sol Author verified AI-led mathematics
2026-08-27 Not every Heyting algebra is the subterminal lattice of a topos Independent ChatGPT 5.6 Sol Author verified AI-assisted mathematics
2026-08-26 Counterexample to Nevanlinna's half-plane omitted-values question Independent GPT-5.6 Sol Ultra Author verified AI-led mathematics
2026-08-25 Improved algebraic construction for off-diagonal Ramsey numbers Independent ChatGPT 5.6 Author verified AI-assisted mathematics
2026-08-25 Improved lower bound for large gaps between consecutive primes Independent GPT-5.6 Sol Independently checked AI-led mathematics
2026-08-25 Sparse domination implies convex body domination Independent GPT-5.6 Sol Pro Author verified AI-assisted mathematics
2026-08-25 Equivalence of generic stability notions for Keisler measures Independent ChatGPT 5.5; ChatGPT 5.6 Sol; Kimi K3; Claude Fable 5 Author verified AI-led mathematics
2026-08-25 Fröberg's conjecture for quintics and septics in four variables Independent GPT-5.6 Sol; Claude Fable 5; Grok 4.6 Author verified Collaborative mathematics
2026-08-23 A proposed complex structure on the six-sphere Anthropic Claude, version not stated Claimed AI-assisted mathematics
2026-08-23 Elliptic curves over the rationals of rank at least 30 and at least 31 Independent Claude Claimed AI-assisted mathematics
2026-08-22 Transcendence in the affine case of Erdős Problem 270 Independent GPT-5.6 Sol (Codex) Claimed AI-led mathematics
2026-08-21 Dubickas's question on integral parts of powers of square roots settled Independent Claude Fable 5 and Claude Opus 5 Formally verified AI-led mathematics
2026-08-21 Stable commutator length of a relator is not a one-relator group invariant Independent Claude Opus 5; Harmonic Aristotle Author verified AI-assisted mathematics
2026-08-21 Counterexample to the bounded mass property on the Hopf threefold Independent Rethlas agent (GPT-5.6 Sol) Author verified AI-led mathematics
2026-08-20 A smooth random fast dynamo on the three-torus Independent ChatGPT 5.6 Sol Ultra Author verified AI-led mathematics
2026-08-19 Counterexample to the Yau–Tian–Donaldson conjecture for constant scalar curvature metrics Independent Claude Fable 5, GPT-5.6-sol and Danus Author verified Collaborative mathematics
2026-08-19 Counterexample to the smooth Carathéodory conjecture on umbilic points Independent Claude; Codex Claimed AI-assisted mathematics
2026-08-19 First open case of the big-line-big-clique conjecture Independent GPT-5.6 Sol Pro Author verified AI-led mathematics
2026-08-19 Erdős Problem #501 shown independent of ZFC, with both directions in Lean Independent Sol; Claude Formally verified Collaborative mathematics
2026-08-19 The DeLaViña-Waller conjecture on the Wiener index Independent GPT-5.6 Sol; Claude Fable 5 Author verified AI-assisted mathematics
2026-08-19 Partial proof of the Kasami APN triple-count conjecture, verified in Lean Independent Claude Fable 5; Harmonic Aristotle Formally verified AI-led mathematics
2026-08-18 Bounded prime gaps of 246 formalized in Lean from Bombieri-Vinogradov Axiom Math AxiomProver Formally verified Collaborative mathematics
2026-08-18 Dimension-free weak-type bound for the vector Riesz transform Independent GPT-5.6 Sol and Claude Opus 5.0, with Danus and Rethlas agents Author verified Collaborative mathematics
2026-08-16 Talagrand's convolution conjecture proved on the Boolean hypercube Independent Odin Automatic AI Research Agent Author verified AI-led mathematics
2026-08-13 SOP_2 and SOP_3 theories shown to coincide Independent ChatGPT 5.6 Author verified Collaborative mathematics
2026-08-13 Banach's isometric conjecture settled in the remaining odd dimensions Independent ChatGPT 5.5 Pro, ChatGPT 5.6 Pro and GPT-5.6 Sol Author verified AI-assisted mathematics
2026-08-12 Complete minimizer picture for Gamow's liquid drop model Independent ChatGPT 5.6 Pro Author verified AI-led mathematics
2026-08-10 Proportion of zeta zeros on the critical line raised to 67.25% Anthropic Claude (unreleased research version) Formally verified AI-led mathematics
2026-08-08 A 112-vertex counterexample to the Petersen coloring conjecture Independent Unnamed OpenAI model Formally verified AI-assisted mathematics
2026-08-06 Separation between the ordinary and strong Kreiss constants Independent ChatGPT 5.6 Pro; Claude Fable Author verified AI-assisted mathematics
2026-08-05 Sendov's conjecture proved for every degree Independent GPT-5.6 Pro Formally verified Collaborative mathematics
2026-08-05 Counterexamples to Schiffer's conjecture and the Pompeiu problem Independent GPT-5.6, Claude Opus 4.8, Claude Fable 5 Formally verified AI-assisted mathematics
2026-08-04 Asymptotic degree-diameter problem resolved for fixed diameter Independent GPT-5.6 Pro Formally verified AI-assisted mathematics
2026-08-01 Ten results in mathematics and theoretical computer science with Lean certificates OpenAI Astra Formally verified AI-led mathematics
2026-07-29 Optimal exponent relating sumsets and difference sets determined Tencent Hunyuan Hy3 (Hyra research agent) Formally verified AI-led mathematics
2026-07-27 Feige's conjecture on sums of nonnegative random variables settled Independent ChatGPT 5.6 Pro Formally verified AI-led mathematics
2026-07-20 Counterexamples to the Gaussian moments conjecture Independent GPT-5.6 Sol Pro + Claude Fable 5 Author verified AI-led mathematics
2026-07-20 Eight problems from the Kourovka Notebook solved and formalized in Lean Harmonic Aristotle Formally verified Autonomous mathematics
2026-07-20 Gaussian product inequality conjecture proved Independent ChatGPT 5.6 Sol Formally verified AI-led mathematics
2026-07-19 Counterexample to the Jacobian conjecture in dimension three Anthropic Claude Fable 5 Formally verified Collaborative mathematics
2026-07-14 Near-quadratic lower bound for derivative-free convex optimization Independent GPT-5.6 Sol Pro Formally verified AI-led mathematics
2026-07-14 Sabidussi's compatibility conjecture proved Independent GPT-5.6 Pro, GPT-5.6 Sol Formally verified Collaborative mathematics
2026-07-11 Counterexample to Grothendieck's question on finite flat group schemes Independent OpenAI Sol (construction); Claude Fable (Lean formalisation) Formally verified Collaborative mathematics
2026-07-10 Cycle double cover conjecture proved for all bridgeless multigraphs OpenAI GPT-5.6 Sol Ultra Formally verified AI-led mathematics
2026-05-21 Nine Erdős problems and 44 OEIS conjectures proved with machine-checked proofs Google DeepMind AlphaProof Nexus (LLM + Lean) Formally verified Search scaffold mathematics
2026-05-20 Disproof of the Erdős unit-distance conjecture OpenAI GPT-5 series reasoning model Independently checked AI-led mathematics
2026-01-15 Structure in Bruhat intervals of permutation groups Google DeepMind AlphaEvolve (Gemini-based) Independently checked Search scaffold mathematics
2026-01-13 Erdős problem #728 resolved and formalized in Lean OpenAI / Harmonic GPT-5.2 Pro + Aristotle Formally verified Autonomous mathematics
2025-11-03 AlphaEvolve across 67 problems: 20 improvements, 8 regressions Google DeepMind AlphaEvolve (Gemini-based) Independently checked Search scaffold mathematics
2025-10-19 GPT-5 "solved 10 Erdős problems": it located existing solutions OpenAI GPT-5 Already known Retrieval mathematics
2025-09-17 New families of unstable singularities in fluid equations Google DeepMind (with Brown, NYU and Stanford) Physics-informed neural networks with Gauss–Newton optimisation Author verified Search scaffold mathematics
2025-09-11 Strong prime number theorem formalized in Lean by an autoformalization agent Math, Inc. Gauss (autoformalization agent) Author verified AI-assisted mathematics
2025-08-01 Improved step-size bound in smooth convex optimization OpenAI GPT-5 Pro Already known AI-assisted mathematics
2025-07-28 Machine-checked Lean proofs for five of six 2025 IMO problems Harmonic Aristotle Formally verified AI-led mathematics
2025-07-21 Gold-medal standard at the 2025 International Mathematical Olympiad Google DeepMind Gemini Deep Think (advanced version) Independently checked AI-led mathematics
2025-05-14 Improved lower bound for the 11-dimensional kissing number Google DeepMind AlphaEvolve (Gemini-based) Independently checked Search scaffold mathematics
2025-05-14 Improved bound for the Erdős minimum-overlap problem Google DeepMind AlphaEvolve (Gemini-based) Independently checked Search scaffold mathematics
2024-07-25 Silver-medal standard at the 2024 International Mathematical Olympiad Google DeepMind AlphaProof + AlphaGeometry 2 Independently checked AI-led mathematics
2024-01-17 Olympiad geometry solved without human demonstrations Google DeepMind AlphaGeometry Peer reviewed Search scaffold mathematics
2023-12-14 New lower bound constructions for the cap set problem Google DeepMind FunSearch (PaLM 2 / Codey) Peer reviewed Search scaffold mathematics
2021-12-01 Two theorems found by machine pattern-spotting in knot theory and representation theory Google DeepMind (with Oxford and Sydney) Supervised networks with gradient-based attribution Peer reviewed AI-assisted mathematics
2021-04-29 Reinforcement learning refutes several conjectures in extremal combinatorics Tel Aviv University Deep cross-entropy method (custom network) Independently checked Search scaffold mathematics

← The whole registry