By verification grade
46 of 123 carry an independent check. Open the review queue.
Open longest before falling
- 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
- 331 yrImproved lower bound for the 11-dimensional kissing numberposed 1694 · AlphaEvolve (Gemini-based)
- 177 yrBounded prime gaps improved to 212, with a Lean certificate of the deductionposed 1849 · AxiomProver
- 177 yrPrime gaps at most 186, conditional on three unproved Lean axiomsposed 1849 · GPT-6 Astra
From the 70 of 123 entries recording a posed year. Add a missing one.
| Date | Finding | Lab | Model | Verification | Autonomy | Field |
|---|---|---|---|---|---|---|
| 2026-10-29 | Lean formalization of interior gradient Hölder estimates for infinity-harmonic functions | Independent | Claude, under the Trellis AI-assisted formalization pipeline; the underlying manuscript came from an unreleased internal OpenAI model | Formally verified | AI-led | mathematics |
| 2026-10-27 | Measurably isomorphic Bernoulli shifts with different base entropies, proved in Lean | Independent | GPT-6 Astra and GPT-6 Sol via Codex, building on an OpenAI construction | Formally verified | Collaborative | mathematics |
| 2026-10-26 | Classification of Finite Simple Groups formalized in Lean by directed AI agents | Axiom Math | AxiomProver agent system using an unnamed, changing mix of models | Claimed | Collaborative | mathematics |
| 2026-10-26 | Sogge's local smoothing conjecture claimed in every dimension, with Bochner–Riesz and Kakeya as consequences | OpenAI | Unreleased internal OpenAI model, not named in the release | Claimed | AI-led | mathematics |
| 2026-10-20 | Lean formalization of the L³ bound for the trilinear Hilbert transform | Independent | GPT-6 Astra Pro for the blueprint, with GPT-6 Astra Light and Claude Opus 5.5 autoformalizing the proof | Formally verified | AI-led | mathematics |
| 2026-10-19 | Erdős Problem 173: a two-coloring of the plane misses at most one triangle, which is equilateral | Plasma AI | GPT-6 Astra (Codex) and Claude Opus 5.5 (Claude Code), alternating; Claude Opus 5.5 (Lean formalization) | Formally verified | AI-led | mathematics |
| 2026-10-19 | Erdős Problem 111: graphs that are not countably colorable need superlinear deletions to become bipartite | Plasma AI | GPT-6 Astra (Codex) and Claude Opus 5.5 (Claude Code), alternating; Claude Opus 5.5 (Lean formalization) | Claimed | AI-led | mathematics |
| 2026-10-19 | Erdős Problem 408: an unconditional normal order for the number of totient iterations | Plasma AI | Claude Opus 5.5 (Lean formalization); the argument is credited to Plasma AI without naming a model | Formally verified | AI-assisted | mathematics |
| 2026-10-18 | Pointwise convergence of ergodic averages along two commuting transformations | Independent | GPT-6 Astra Pro (proof and blueprint); Claude Opus 5.5 (Lean formalization) | Formally verified | AI-led | mathematics |
| 2026-10-18 | Épi agent reports 120 record bounds and constructions, with released certificates | Bake AI | GPT-5.6 Sol and GPT-6 Astra in the Épi agent | Claimed | Search scaffold | mathematics |
| 2026-10-12 | No zeros of any Dedekind zeta function with real part above 31/32, machine-checked in Lean | Axiom Math | AxiomProver | Formally verified | Collaborative | mathematics |
| 2026-10-09 | Strict Pólya inequalities claimed for simply connected planar domains, Dirichlet and Neumann, with Lean formalizations | Independent | ChatGPT for the mathematics, version not stated; Aristotle (Harmonic) and Codex for the Lean | Claimed | AI-assisted | mathematics |
| 2026-10-08 | Lambert series values, including the Erdős-Borwein constant, are not quadratic irrationals | Independent | Generative AI, not named in the repository | Claimed | AI-led | mathematics |
| 2026-10-06 | 719 manuscripts in 372 result families from an unreleased OpenAI model | OpenAI | Unreleased internal OpenAI model, not named in the release | Claimed | AI-led | mathematics |
| 2026-10-06 | Quasi-Riemann hypothesis: no zeros of zeta or any Dirichlet L-function with real part above 7/8 | OpenAI | Unreleased internal OpenAI model, not named in the release | Claimed | Collaborative | mathematics |
| 2026-10-06 | Kakeya maximal conjecture in three dimensions and the Kakeya set conjecture in four | OpenAI | Unreleased internal OpenAI model, not named in the release | Claimed | AI-led | mathematics |
| 2026-10-06 | Counterexample to the Borel conjecture in dimension four | OpenAI | Unreleased internal OpenAI model, not named in the release | Claimed | AI-led | mathematics |
| 2026-10-06 | Artin's primitive root conjecture: infinitely many primes for every admissible base | OpenAI | Unreleased internal OpenAI model, not named in the release | Claimed | AI-led | mathematics |
| 2026-10-06 | Modularity of every elliptic curve over every imaginary quadratic field | OpenAI | Unreleased internal OpenAI model, not named in the release | Claimed | AI-led | mathematics |
| 2026-10-06 | Negative answer to the hyperinvariant subspace problem on Hilbert space | OpenAI | Unreleased internal OpenAI model, not named in the release | Claimed | AI-led | mathematics |
| 2026-10-06 | Massive continuum limit of the two-dimensional O(3) model | OpenAI | Unreleased internal OpenAI model, not named in the release | Claimed | AI-led | mathematics |
| 2026-10-06 | Proof of Barnette's conjecture on Hamiltonian cycles in cubic bipartite planar graphs | OpenAI | Unreleased internal OpenAI model, not named in the release | Claimed | AI-led | mathematics |
| 2026-10-06 | Shelah's eventual categoricity conjecture for abstract elementary classes | OpenAI | Unreleased internal OpenAI model, not named in the release | Claimed | AI-led | mathematics |
| 2026-10-04 | Kannan–Lovász–Simonovits conjecture proved in two preprints posted the same day | Independent | ChatGPT, version not stated (Bizeul, Klartag and Lehec); GPT-6 Astra, GPT-5.6 Sol, Claude Fable 5 and Fable 5.1 (Song and Zhang) | Collaborative | mathematics | |
| 2026-10-02 | Optimal packings of one to seven unit squares in a circle, proved in Lean | Independent | ChatGPT (GPT-6 Pro) and Claude Opus 5 and 5.5 | Formally verified | AI-led | mathematics |
| 2026-10-01 | Closed form for the anisotropic Watson integral of the cubic lattice | Independent | Claude (the announcement names Claude Fable 5) | Claimed | AI-assisted | mathematics |
| 2026-09-26 | Erdős Problem #1220 formalized as not provable in ZFC, from a 1987 Shelah-Stanley consistency result | Independent | Claude Opus 5.5 (Claude Code); Astra (OpenAI Codex) | AI-assisted | mathematics | |
| 2026-09-26 | Hamilton cycles in connected Cayley graphs of polylogarithmic degree, toward the Lovász conjecture | Independent | GPT 6 Pro (manuscript draft); Claude Opus 5.5 agents in Grok Build (Lean formalization) | Claimed | Collaborative | mathematics |
| 2026-09-17 | Counterexample to Talagrand's operator cotype problem | Independent | ChatGPT (GPT-5.6) | Claimed | AI-led | mathematics |
| 2026-09-17 | Huang-Jiang-Oblomkov conjecture proved for every torus-knot singularity, with a Lean formalization conditional on two literature inputs | Axiom Math | AxiomProver | Claimed | AI-assisted | mathematics |
| 2026-09-16 | Browning-Sawin conjecture on random sign-coefficient hypersurfaces proved, with a Lean formalization assuming existing literature | Axiom Math | AxiomProver | Claimed | AI-assisted | mathematics |
| 2026-09-16 | Four Color Theorem formalized in Lean 4 by AI agents, in two independent developments | Independent | Claude Fable 5.1 and Claude Opus 5 (Emery); Claude Opus 5.5 (Barish) | Claimed | AI-led | mathematics |
| 2026-09-15 | Finite-time blowup for the IPM equation with uniformly space-time smooth forcing | Independent | Not named; the arXiv comment field states only that the proof is LLM-assisted | Claimed | AI-assisted | mathematics |
| 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-14 | Eight open problems from Formal Conjectures proved in Lean by a simple agent loop | FAIR at Meta | GPT-5.6 Sol in the h1 harness | Formally verified | Search scaffold | mathematics |
| 2026-09-10 | Existence of the core in approval-based committee elections | Independent | GPT-6 Astra | Claimed | Collaborative | mathematics |
| 2026-09-09 | A 3-generator 9-relator group with unsolvable word problem, and smaller Adian-Rabin families | Independent | GPT-5.6 Sol Pro (construction); GPT-5.6 Sol in Codex (Lean formalization) | 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-07 | Improved lower bound for the complex Grothendieck constant | Independent | Odin Automatic AI Research Agent | 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) | Formally verified | 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 | AI-led | mathematics | |
| 2026-09-02 | A smooth counterexample to the Trautman conjecture | Oklahoma State University | ChatGPT Plus, version not named | 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 | 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 | 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 | AI-led | mathematics | |
| 2026-08-27 | Not every Heyting algebra is the subterminal lattice of a topos | Independent | ChatGPT 5.6 Sol | AI-assisted | mathematics | |
| 2026-08-27 | Norm-variation of multiple ergodic averages, including Tao's norm-convergence theorem, autoformalized in Lean in one week | Independent | Coding agents, models not stated | AI-led | mathematics | |
| 2026-08-27 | Proof of the Lyons–White conjecture on rate-monotonic random walks | Axiom Math | AxiomProver | Formally verified | AI-assisted | mathematics |
| 2026-08-26 | Counterexample to Nevanlinna's half-plane omitted-values question | Independent | GPT-5.6 Sol Ultra | Formally verified | AI-led | mathematics |
| 2026-08-25 | Improved algebraic construction for off-diagonal Ramsey numbers | Independent | ChatGPT 5.6 | 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 | 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 | 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 | Collaborative | mathematics | |
| 2026-08-23 | A complex structure on the six-sphere | Anthropic | Claude, version not stated | Independently checked | 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 | AI-assisted | mathematics | |
| 2026-08-21 | Counterexample to the bounded mass property on the Hopf threefold | Independent | Rethlas agent (GPT-5.6 Sol) | AI-led | mathematics | |
| 2026-08-20 | A smooth random fast dynamo on the three-torus | Independent | ChatGPT 5.6 Sol Ultra | 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 | 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 | 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 | 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 | Collaborative | mathematics | |
| 2026-08-16 | Talagrand's convolution conjecture proved on the Boolean hypercube | Independent | Odin Automatic AI Research Agent | AI-led | mathematics | |
| 2026-08-13 | SOP₂ and SOP₃ theories shown to coincide | Independent | ChatGPT 5.6 | 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 | AI-assisted | mathematics | |
| 2026-08-12 | Complete minimizer picture for Gamow's liquid drop model | Independent | ChatGPT 5.6 Pro | 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 | AI-assisted | mathematics | |
| 2026-08-06 | Huang-Jiang-Oblomkov conjecture for a = 3: a new infinite family of Rogers-Ramanujan identities, with a Lean certificate conditional on eight literature facts | Axiom Math | AxiomProver | Claimed | 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 | 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-29 | Erdős Problem 654 answered negatively by Google DeepMind's Aletheia agent | Google DeepMind | Aletheia, a mathematics research agent built on Gemini Deep Think | 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 | Search scaffold | mathematics | |
| 2025-09-11 | Strong prime number theorem formalized in Lean by an autoformalization agent | Math, Inc. | Gauss (autoformalization agent) | 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 |