AI-assisted claims

Partial result claimed · 29 Oct 2026

An improved zero-free half-plane for Hecke L-functions over number fields and Quasi-Riemann Hypothesis

“In this paper, we obtain a zero-free half-plane Re(s) > B∗ for every finite-order Hecke L-function over every number field, where B∗ = 0.87446830769353045955... is an explicitly defined algebraic number. This improves the Quasi-Riemann Hypothesis over arbitrary number fields.”

By

Baiying Liu

AI involvement

Text declaration: A mix of human-written and AI-generated. Human-understanding declaration: Some parts of this contribution, but not all, have been checked and understood by a human. Additional provenance: OpenAI Codex (GPT 6.1 Sol Medium-Ultra) and Anthropic Claude (Opus 5.5 Medium) assisted with drafting, checking references, the search for improved bounds, and auditing. The Lean formalization is in progress, based on the Lean files in [Liu26c] and in [CTLean].

Model

OpenAI Codex (GPT 6.1 Sol Medium-Ultra); Anthropic Claude (Opus 5.5 Medium), as stated

Where

Hexagon

Checked

30 Oct 2026

Partial result claimed · 14 Oct 2026

A quasi-Riemann hypothesis for Dedekind zeta functions

“Following their strategy, we prove that if K is any number field, then the Dedekind zeta function ζ_K(s) does not vanish in the half-plane Re s > 31/32.”

By

Dean Cureton, Jesse Thorner

AI involvement

Text declaration: A mix of human-written and AI-generated. Human-understanding declaration: Some parts of this contribution, but not all, have been checked and understood by a human. Additional provenance: The proofs and Lean formalization were generated by AxiomProver.

Model

AxiomProver, as stated

Where

Hexagon

Formal proof

Lean, published by the source

Checked

29 Oct 2026

Partial result claimed · 06 Oct 2026

The Quasi-Riemann Hypothesis

“We establish the quasi-Riemann hypothesis by proving that every Dirichlet L-function, including Riemann's zeta function, has no zeros in the half-plane Re s > 11/12. More generally, we prove the same zero-free half-plane for every finite-order Hecke L-function over K = Q(√−3). In particular, this rules out the existence of Landau–Siegel zeros.”

By

OpenAI

AI involvement

Exceptions to this fixed procedure include work on a zero-free region for the Riemann zeta function and proof of the Hodge Conjecture for CM abelian varieties. Additionally, the writeup for the Re(s) > 11/12 zero-free region for the Riemann zeta function was human edited for readability. … This paper was written with human assistance.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Checked

14 Oct 2026

Partial result claimed · 06 Oct 2026

The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s)>7/8

“In particular, Theorem 1.1 resolves the quasi-Riemann hypothesis affirmatively: the supremum of the real parts of the nontrivial zeros of ζ, namely its zeros in 0 < ℜs < 1, is at most 7/8. The boundary ℜs = 7/8 is not included, while any exceptional real zero in (7/8, 1) is excluded. The theorem does not establish the Riemann hypothesis or its generalized versions, which place nontrivial zeros on ℜs = 1/2.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model. … Exceptions to this fixed procedure include work on a zero-free region for the Riemann zeta function and proof of the Hodge Conjecture for CM abelian varieties.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Formal proof

Lean 4, published by the source

Checked

14 Oct 2026

Updates

• 08 Oct 2026 · Response · Baiying Liu: “Recently, a uniform 7/8 zero-free half-plane for finite-order Hecke L-functions over Q(√−3) and its transfer to Dirichlet L-functions was given by OpenAI in [Ope26a]. In its proof, there are several parameters b = 1/8, ℓ = 1/6, and κ. In this paper, via varying b, ℓ, and κ, following the same strategy, we slightly improve the bound 7/8 = 0.875 to B_new = (18ξ_new + 7)/(18ξ_new + 9) = 0.874957019420098946…”
• 08 Oct 2026 · Response · Frank Calegari: “Perhaps my point of view was that these represented something close to the limits of analytic arguments, and that one would need a more algebraic perspective to make a truly significant improvement. Obviously, I was totally wrong, and something was clearly missed. But I have no idea of the structure of what is going on. I still believe, although perhaps with slightly less conviction, that improvements to these analytic arguments are not going to be sufficient to prove the full Riemann hypothesis.”

Partial result claimed · Revised · 10 Aug 2026

Learning more about Claude's mathematical capabilities

“An unreleased research version of Claude has improved on a longstanding lower bound for the fraction of zeros of the Riemann zeta function that satisfy the Riemann hypothesis. Drawing on extensive prior research by mathematicians over the past decades, it has increased this bound from 41.6% to 67.2%.”

By

Anthropic

AI involvement

An unreleased research version of Claude found the new lower bound over two sessions in Claude Code, using a total of 31 million output tokens. The paper is credited to “Claude, Anthropic”; its arXiv version (2608.13637) is listed under Levent Alpöge and Ralph Furman.

Model

an unreleased research version of Claude, as stated

Where

Anthropic website (research post)

Formal proof

Lean 4, published by the source

Checked

14 Oct 2026

Updates

• 13 Aug 2026 · Revised by Anthropic: “this post was updated on August 13, 2026, with an updated version of Claude's paper. This paper was revised by Claude to provide a clearer proof and additional historical context.”
• 02 Sep 2026 · Response · Youness Lamzouri: “The argument produced by Claude is technically intricate, and its main mechanism is not immediately transparent. It combines several ingredients from linear algebra, including a finite-dimensional matrix representation of Weil's Hermitian form and a rank–trace inequality for Hermitian matrices, with a second moment calculation over the zeros using the explicit formula. Our new approach proceeds by replacing the entire finite-dimensional matrix framework by a single Hilbert space inequality, which allows for a direct application of Montgomery's theorem on the pair correlation of zeros of the zeta function, in the unconditional form obtained by Baluyot, Goldston, Suriajaya and Turnage-Butterbaugh.”

Disproof claimed · 26 Oct 2026

A 2^o(n) Time Algorithm for 3-SAT

“We refute the Exponential Time Hypothesis (ETH) by presenting a deterministic algorithm for 3-SAT on n variables that runs in 2^o(n) time. Our algorithm in fact solves the harder problem #3-SAT, providing a count of the number of satisfying assignments.”

By

Anthropic

AI involvement

The core algorithm was found on October 16 by an internal Claude research model with 14M output tokens and no human input. Anthropic researchers worked with Claude to improve the presentation, resulting in this paper. Independently and concurrently, an internal model at OpenAI claims to have proven a similar result.

Model

an internal Claude research model, as stated

Where

anthropics/formal-math repository

Write-up

Natural language, published by the source

Formal proof

Lean 4, published by the source

Checked

27 Oct 2026

Disproof claimed · 26 Oct 2026

The Exponential Time Hypothesis is false

“Surprisingly, our system has recently proved that the ETH is false, a result that was subsequently verified in Lean.”

By

OpenAI

AI involvement

Our AI found its natural language disproof for the ETH on October 16th, 2026 and then subsequently we formalized the result in Lean on October 17th, 2026

Model

internal OpenAI models, as stated

Where

OpenAI announcement

Write-up

Natural language, published by the source

Formal proof

Lean 4, published by the source

Verifying

A group led by Russell Impagliazzo (UC San Diego), Ramamohan Paturi (UC San Diego) and Ryan Williams (MIT)

Checked

27 Oct 2026

Note: Refuting ETH does not resolve P vs NP.

Updates

• 28 Oct 2026 · Response · Chelsea Anne McElveen, in the community repository oai-math-revised: “NOTES.md — commentary: an executable model of Sections 2.3–2.7 checked against brute force at n ≤ 14; two structural remarks on the Section 2.7 construction … Does not change the TeX source or the manuscript's claims. No error in the manuscript is asserted.”

Partial result claimed · 26 Oct 2026

Existence of quantum chromodynamics and completions of the Standard Model

“As a subproblem, this work also includes a proof of the existence of pure Yang–Mills theory, which is part of the Quantum Yang–Mills Theory Clay Mathematics Institute Millennium Prize problem.”

By

OpenAI

AI involvement

Our models produced a natural language proof for Yang–Mills existence on September 9th, 2026, and then subsequently produced a proof for QCD on September 18th, 2026.

Model

internal OpenAI models, as stated

Where

OpenAI announcement

Checked

27 Oct 2026

Note: OpenAI reports an AI-produced existence proof for pure Yang–Mills and QCD in 4D (Oct 2026), shepherded by a group led by David Gross. The mass gap is not addressed. AI artifacts not yet released.

Updates

• 26 Oct 2026 · Response · AGMAI: “We call on OpenAI to make public without delay the natural-language and Lean outputs behind its announced existence proofs for Yang–Mills theory, quantum chromodynamics, and a completion of the Standard Model.”
• 28 Oct 2026 · Response · Shepherding committee: Michael R. Douglas, David J. Gross (Chair), Arthur Jaffe, Igor R. Klebanov, Nikita Nekrasov: “Balaban’s ideas were among the important elements that recently enabled OpenAI to follow the theory all the way to infinite distances and prove the existence of its proper continuum limit. But confinement and the mass gap remain very important open challenges. … Before we release it, we would like to be convinced that it is correct. … Once this validation is done, we will release the Lean proof.”

Partial result claimed · 15 Oct 2026

Yang–Mills LLM experiment

“This repository contains a manuscript [QED3] which, if correct, contains a full construction of quantum electrodynamics in three dimensions (QED3), in infinite volume. … For Yang–Mills in three-dimensions (YM3), we have a manuscript [YMM1] which, if correct, contains a verification of the Osterwalder–Schrader axioms for tr[F²].”

By

Ethan Sussman, Levent Alpöge

AI involvement

This repository contains work-in-progress, written largely by LLM. … Novel mathematical ideas should be attributed to Claude (under the guidance of LA). … The manuscripts cited above are the result of cutting material from literally thousands of pages of slop generated by Claude. … It is then fed to Codex to extract a minimal manuscript.

Model

Claude; Codex, as stated

Where

GitHub repository ethanwsussman/Yang--Mills-LLM-experiment

Checked

30 Oct 2026

Note: The repository's README calls all its claims "tentative, pending verification". The results stated are in three dimensions (QED3, YM3); on four dimensions it says only that they "appear to" have an existence argument. The mass gap is not addressed.

Partial result claimed · 26 Oct 2026

Positive density of Collatz convergence at every rate above 3/log(4/3)

“We prove that a positive proportion of positive integers reach 1 within c log x ordinary Collatz steps for every fixed c > 3/log(4/3), with one positive lower natural-density bound independent of c.”

By

Idris Ali Shaik

AI involvement

Text declaration: A mix of human-written and AI-generated. Human-understanding declaration: All parts of this contribution have been checked and understood by a human. Additional provenance: AI-assisted tools were used in manuscript preparation, Lean proof development, code preparation, and editorial revision.

Where

Hexagon

Formal proof

Lean, published by the source

Checked

27 Oct 2026

Partial result claimed · 21 Oct 2026

Explicit positive lower density for the Collatz Conjecture

“For every N, at least ⌊N/2^(2^(2^163))⌋ odd positive integers n < N reach 1 within 10.46 log n ordinary steps and 3.4881 log n accelerated steps.”

By

Kenny Lau

AI involvement

Text declaration: A mix of human-written and AI-generated. Human-understanding declaration: Some parts of this contribution, but not all, have been checked and understood by a human. Additional provenance: This project was born out of our goal to formalize Mazur's paper, with the intent of improving the estimates. With this stated goal, AxiomProver autonomously produced the mathematics in this paper and formalized it in Lean.

Model

AxiomProver, as stated

Where

Hexagon

Formal proof

Lean, published by the source

Checked

27 Oct 2026

Partial result claimed · 17 Oct 2026

Polylogarithmic Descent for Almost All Collatz Orbits in Natural Density

“We obtain polylogarithmic descent in ordinary natural density within logarithmically many steps, with bounds on the preceding orbit values.”

By

Idris Ali Shaik

AI involvement

Text declaration: A mix of human-written and AI-generated. Human-understanding declaration: All parts of this contribution have been checked and understood by a human. Additional provenance: OpenAI Codex assisted with mathematical exploration, Lean formalization, and manuscript preparation. The author reviewed the AI-assisted material and takes full responsibility for the manuscript.

Model

OpenAI Codex, as stated

Where

Hexagon

Formal proof

Lean, published by the source

Checked

27 Oct 2026

Partial result claimed · 22 Oct 2026

Algebraicity of Weil classes on abelian sixfolds of Weil type for ℚ(√−3) with discriminant −2

“We prove that the Weil classes of every polarized abelian sixfold of Weil type for K = ℚ(√−3) with Hermitian discriminant −2 are algebraic.”

By

Benjamin Severn

AI involvement

Text declaration: Primarily AI-generated. Human-understanding declaration: Some parts of this contribution, but not all, have been checked and understood by a human. Additional provenance: This paper was produced in a research programme directed by the author, in which AI systems did most of the mathematical derivation, the computer-algebra code and the writing.

Model

Claude Opus 5.5, Claude Sonnet 5.5; Codex (GPT-5.6 Sol, GPT-6 Astra, GPT-5.6 Luna), as stated

Where

Hexagon

Checked

27 Oct 2026

Partial result claimed · 22 Oct 2026

Weil classes on every abelian sixfold of Weil type for ℚ(√−3)

“We prove that the Weil classes of every polarized complex abelian sixfold of Weil type for K = ℚ(√−3), of every Hermitian discriminant, are algebraic.”

By

Benjamin Severn

AI involvement

Text declaration: Primarily AI-generated. Human-understanding declaration: Some parts of this contribution, but not all, have been checked and understood by a human. Additional provenance: This paper was produced in a research programme directed by the author, in which AI systems did most of the mathematical derivation, the computer-algebra code and the writing.

Model

Claude Opus 5.5, Claude Sonnet 5.5; Codex (GPT-6 Astra, GPT-5.6 Sol, GPT-5.6 Luna), as stated

Where

Hexagon

Checked

27 Oct 2026

Partial result claimed · 18 Oct 2026

The Hodge Conjecture for CM abelian varieties

“Following the recent work [Ope26], we give a proof of the Hodge conjecture for CM abelian varieties.”

By

Pol van Hoften, Jack Sempliner

AI involvement

Text declaration: Primarily human-written. Human-understanding declaration: All parts of this contribution have been checked and understood by a human. Additional provenance: This article is entirely human written. That said, we made extensive use of ChatGPT Pro during the preparation of this argument.

Model

ChatGPT 6.1, as stated

Where

Hexagon

Checked

27 Oct 2026

Partial result claimed · 06 Oct 2026

Abelian covers, Gale correspondences, and the Hodge conjecture for powers

“We prove the rational Hodge conjecture on every self-power of the Jacobian at each tensor Hodge-generic point of the full marked variation of a connected abelian cover of curves. This holds in every base genus and for every compatible branching pattern.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Checked

14 Oct 2026

Partial result claimed · 06 Oct 2026

Algebraic Kuga–Satake correspondences and Hodge conjectures on a K3 quadratic locus

“We prove the rational Hodge and generalized Hodge conjectures in every cohomological degree of every self-power of a projective complex K3 surface whose transcendental quadratic space, with its cup-product form, admits a rational isometric embedding in U_Q^{⊕2} ⊥ ⟨−1⟩^4. This includes every ample P-polarized K3 surface, including all Picard jumps, for P = U ⊕ D8(−1) ⊕ D4(−1).”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Checked

14 Oct 2026

Partial result claimed · Withdrawn · 06 Oct 2026

Algebraicity of Kuga–Satake Correspondences for K3 Surfaces

“We prove that the Kuga–Satake correspondence is algebraic for every smooth projective complex K3 surface. More precisely, the prescribed embedding of its transcendental cohomology into the cohomology of its Kuga–Satake abelian variety is induced by a rational algebraic cycle, with the fixed normalization and full even-Clifford target.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Checked

14 Oct 2026

Updates

• 06 Oct 2026 · Withdrawn by OpenAI: “The proof relies on an adaptation of the flawed stabilization-trace construction in Algebraicity of Weil classes on split abelian eightfolds. The sign error in that construction prevents the required signed-double-point cancellation. The resulting gap leaves this paper's claimed algebraicity theorem unproved. This withdrawal concerns the proof; it does not assert that the mathematical statement is false.”
• 22 Oct 2026 · Response · Yankı Lekili, Nick Sheridan: “The documents [OAI26a, OAI26b, OAI26c] claimed to prove cases of the Hodge conjecture via homological mirror symmetry, before being withdrawn by OpenAI. We discuss the source of the error (but do not analyse the rest of the argument).”

Partial result claimed · Withdrawn · 06 Oct 2026

Algebraicity of Weil classes on split abelian eightfolds

“The Weil classes are a particularly concrete test of the Hodge conjecture: they form a rational two-dimensional space defined by an imaginary quadratic action, while their algebraic representatives generally do not come from products of divisor classes. This paper establishes their algebraicity in the split eight-dimensional case.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Checked

14 Oct 2026

Updates

• 06 Oct 2026 · Withdrawn by OpenAI: “The proof contains a sign error in the stabilization-trace argument used to obtain negative double points. … The Eliashberg-Murphy cancellation theorem invoked at this step requires zero signed double-point count, so its hypothesis is not met. The subsequent oriented-surgery and embedded-brane construction is therefore unsupported, and the paper does not establish its claimed algebraicity theorem. This withdrawal concerns the proof; it does not assert that the mathematical statement is false.”
• 22 Oct 2026 · Response · Yankı Lekili, Nick Sheridan: “The documents [OAI26a, OAI26b, OAI26c] claimed to prove cases of the Hodge conjecture via homological mirror symmetry, before being withdrawn by OpenAI. We discuss the source of the error (but do not analyse the rest of the argument).”

Partial result claimed · 06 Oct 2026

The rational Hodge conjecture for CM abelian varieties

“We prove the rational Hodge conjecture for complex abelian varieties with complex multiplication: every rational Hodge class on such a variety is a rational linear combination of algebraic cycle classes. As consequences, we obtain the generalized Hodge conjecture for CM abelian varieties, the Tate conjecture for abelian varieties over finite fields, and the Hodge standard conjecture for abelian varieties in arbitrary characteristic.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model. … Exceptions to this fixed procedure include work on a zero-free region for the Riemann zeta function and proof of the Hodge Conjecture for CM abelian varieties.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Checked

14 Oct 2026

Partial result claimed · Withdrawn · 06 Oct 2026

The rational Hodge conjecture for products of K3 surfaces

“We prove the rational Hodge conjecture for every finite product of projective complex K3 surfaces: every rational Hodge class is algebraic. The factors may be distinct or repeated, with no restrictions on their Picard numbers, periods, or endomorphism fields.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Checked

14 Oct 2026

Updates

• 06 Oct 2026 · Withdrawn by OpenAI: “The proof relies on an adaptation of the flawed stabilization-trace construction in Algebraicity of Weil classes on split abelian eightfolds. The sign error in that construction prevents the required signed-double-point cancellation. The resulting gap leaves this paper's claimed rational Hodge theorem for products of projective K3 surfaces unproved. This withdrawal concerns the proof; it does not assert that the mathematical statement is false.”
• 22 Oct 2026 · Response · Yankı Lekili, Nick Sheridan: “The documents [OAI26a, OAI26b, OAI26c] claimed to prove cases of the Hodge conjecture via homological mirror symmetry, before being withdrawn by OpenAI. We discuss the source of the error (but do not analyse the rest of the argument).”

Partial result claimed · 06 Oct 2026

Weil classes and Hodge classes on abelian powers

“We prove the rational Hodge conjecture in every codimension on every self-power of a complex abelian sixfold with an imaginary-quadratic action and a compatible polarization whose rational homological Hermitian form is hyperbolic of signature (3,3). We also prove it in every codimension on every self-power of a complex abelian variety of dimension at most five admitting an imaginary-quadratic action.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Checked

14 Oct 2026

Partial result claimed · Revised · 10 Oct 2026

Kissing numbers — Preprints and improved kissing number constructions

“We prove that the kissing numbers in 19 and 21 dimensions are at least 12460 and 31560, improving the best published bounds 11948 (Ho) and 29768 (Cohn and Li). … We prove that the kissing numbers in 28, 29, 30 and 31 dimensions are at least 205172, 210495, 222073 and 241079. … We give two kissing configurations of 8358 points in 18 dimensions. This exceeds the best published lower bound, 7654 by Cohn and Li, by 704, and ties a value reported earlier by Kravatskiy in a public repository.”

By

Kevin Li (GitHub: Felpix-Studios)

AI involvement

GPT-6 Astra Pro, Claude Opus 5.5 and Claude Fable 5.1 were used to find these constructions, prepare supplementary data and draft this paper. The manuscript was proofread and lightly revised by the author.

Model

GPT-6 Astra Pro; Claude Opus 5.5; Claude Fable 5.1, as stated

Where

GitHub repository Felpix-Studios/kissing-number

Checked

18 Oct 2026

Updates

• 13 Oct 2026 · Revised by Kevin Li: “bound updates”
• 14 Oct 2026 · Revised by Kevin Li: “Pre-print updates”

Partial result claimed · 05 Oct 2026

New lower bounds for kissing numbers in dimensions 25, 26, 27, 29 and 31

“Starting from constructions based on the Leech lattice, we obtain the improved lower bounds τ25 ≥ 197583, τ26 ≥ 199868, τ27 ≥ 201589, τ29 ≥ 209970 and τ31 ≥ 238666.”

By

Rustem Takhanov, Stanislav Yun

AI involvement

All new constructions were generated with AI systems: Claude Code with Claude Opus 5.5, and GPT-6 Astra.

Model

Claude Code with Claude Opus 5.5; GPT-6 Astra, as stated

Where

GitHub repository k-nic/kissing_d25-31

Checked

14 Oct 2026

Partial result claimed · 02 Oct 2026

A Fourier Consequence for Lattice Kissing Numbers and Average Contacts

“We deduce a new asymptotic upper bound K_lat(n) ≤ (√(2e/π) + o(1))^n on the maximal lattice kissing number K_lat(n) in dimension n, using the explicit auxiliary functions constructed in OpenAI's "Ten Advances" preprint.”

By

Scott Kominers

AI involvement

Text declaration: A mix of human-written and AI-generated. Human-understanding declaration: All parts of this contribution have been checked and understood by a human. Additional provenance: I used LLMs to assist with analysis and synthesis in the preparation of this article, particularly GPT-6 Astra and Claude Fable 5.1 (accessed in part via Poe with the support of Quora, where I am an advisor). In particular, the bound I present was developed in dialogue with GPT-6 Astra.

Model

GPT-6 Astra, Claude Fable 5.1, as stated

Where

Hexagon

Checked

27 Oct 2026

Partial result claimed · Revised · 30 Sep 2026

Improved kissing numbers in nineteen and twenty-one dimensions

“We prove that the kissing numbers in 19 and 21 dimensions are at least 12276 and 30779.”

By

Kevin Li (GitHub: Felpix-Studios)

AI involvement

GPT-6-Astra Pro and Claude Opus 5.5 were used to find these constructions, write the Lean formalization, and draft the paper.

Model

GPT-6-Astra Pro; Claude Opus 5.5, as stated

Where

GitHub repository Felpix-Studios/D19-D21-Kissing

Formal proof

Lean 4, published by the source

Checked

14 Oct 2026

Updates

• 04 Oct 2026 · Revised by Kevin Li: “τ₂₁ ≥ 30779 (best published bound 29768: H. Cohn and A. Li, arXiv:2411.04916).”
• 05 Oct 2026 · Revised by Kevin Li: “D19: tau19 >= 12270 (restore two deleted points)”
• 10 Oct 2026 · Revised by Kevin Li: “τ₁₉ ≥ 12276 (best published bound 11948: B. S. Ho, arXiv:2603.10425),”

Partial result claimed · 28 Sep 2026

Large-Scale Autonomous Discovery of Kissing Number Constructions

“Here we use Qiushi Engine, an autonomous multi-agent research system, to investigate kissing numbers and obtain new lower bounds in nineteen dimensions: 25, 27, 32–39, 43, 45, and 49–55.”

By

Shuxing Yang, Rui Zhao, Junyao Wu, Yize Wang, Fujia Chen, Kaihao Zhu, Wenhao Li, Zichen Li, Yaqi Li, Shenzhan Hong, Yuang Pan, Junjie Yang, Taowen Deng, Jincheng Mi, Hongsheng Chen, Yihao Yang

AI involvement

The autonomous system carried out the construction searches, mathematical analysis and computational verification, while each final result was reduced to explicit mathematical arguments and independently checkable finite certificates.

Model

Qiushi Engine, as stated

Where

arXiv

Checked

14 Oct 2026

Partial result claimed · Revised · 30 Aug 2026

Kissing numbers: new lower bounds in dimensions 18 through 96, with verification packages

“Verification packages for new lower bounds on the kissing number in 53 dimensions: 18, 25-31, 38, 39, 49-63, 68-71 and 73-96.”

By

Alexey Kravatskiy

AI involvement

The constructions, the verification code and the write-ups in this repository were developed by the author working with Claude Code (Anthropic).

Model

Claude Code (Anthropic), as stated

Where

GitHub repository alexlegeartis/KissingNumbers

Checked

14 Oct 2026

Updates

• 07 Sep 2026 · Revised by Alexey Kravatskiy: “Dimension 25: tau(25) >= 197569, the lens-head configuration, replaces the +2 cap-level claim”
• 15 Sep 2026 · Revised by Alexey Kravatskiy: “Dimensions 28 to 31: four new claims, 52 in all; the norm-8 frame layer is 96k points in every dimension”
• 16 Sep 2026 · Revised by Alexey Kravatskiy: “Debugging pass: two claims that had outgrown their scope, and a check that could not fail”

Partial result claimed · Revised · 01 Aug 2026

Ten Advances in Mathematics and Theoretical Computer Science

“The n-dimensional kissing number is τ_n = A(n, 1/2). Already hierarchy level 2 gives τ_n ≤ 2^((0.39661+o(1))n), compared with the optimized classical exponent 0.400944….”

By

OpenAI

AI involvement

The results were achieved by an internal version of Astra, our next major model. … These arguments were then prepared into manuscripts by humans with the same model. Afterward, the model formalized each argument in a Lean certificate.

Model

an internal version of Astra, as stated

Where

OpenAI (paper PDF accompanying the post 'Ten advances in mathematics and theoretical computer science')

Checked

14 Oct 2026

Updates

• 06 Aug 2026 · Revised by OpenAI: “Updated August 6, 2026. The original version can be found at https://cdn.openai.com/pdf/ten-proofs-oai-original.pdf.”

Partial result claimed · Revised · 09 Jun 2026

Harnessing the Collective Intelligence of AI Agents in the Wild for New Discoveries

“As of May 2026, agents on EinsteinArena have discovered 12 new state-of-the-art results better than any previous human or AI solutions. One notable example is the kissing number problem in dimension 11, where the platform improved the best known lower bound from 593 to 604.”

By

Federico Bianchi, Yongchan Kwon, Aneesh Pappu, James Zou

AI involvement

In EinsteinArena, a collaborative effort among AI agents improved this lower bound to 594, after which we had agents build on their result to further extend it to 604.

Where

arXiv

Checked

14 Oct 2026

Updates

• 26 Aug 2026 · Revised by Federico Bianchi, Yongchan Kwon, Aneesh Pappu, James Zou: “Updated to correct a mistake”

Partial result claimed · Revised · 11 Mar 2026

A new lower bound for the kissing number in 19 dimensions

“We prove that the kissing number in 19 dimensions is at least 11948, improving the bound of Cohn and Li by 256.”

By

Boon Suan Ho

AI involvement

GPT-5.4 Pro was used in the discovery of the construction and in revising the exposition.

Model

GPT-5.4 Pro, as stated

Where

arXiv

Checked

14 Oct 2026

Updates

• 20 Mar 2026 · Revised by Boon Suan Ho: “v2: corrected errors and improved exposition; main results unchanged”

Partial result claimed · 17 Nov 2025

Finding Kissing Numbers with Game-theoretic Reinforcement Learning

“Working within extremal configuration spaces, PackingStar discovers new interpretable geometric structures that improve 15 strong bounds held for decades in kissing numbers and their generalizations, several of them provably optimal under natural inner products.”

By

Chengdong Ma, Théo Tao Zhaowei, Pengyu Li, Minghao Liu, Haojun Chen, Zihao Mao, Yuan Cheng, Yuan Qi, Yaodong Yang

AI involvement

Accordingly, we recast this problem as a cooperative matrix-completion game, and train a reinforcement learning system, PackingStar, to solve it. One player fills cosine entries while the other corrects suboptimal ones, making explosive geometric complexity tractable.

Model

PackingStar (reinforcement learning system), as stated

Where

arXiv

Checked

14 Oct 2026

Partial result claimed · 14 May 2025

AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms

“For example, it advanced the kissing number problem. This geometric challenge has fascinated mathematicians for over 300 years and concerns the maximum number of non-overlapping spheres that touch a common unit sphere. AlphaEvolve discovered a configuration of 593 outer spheres and established a new lower bound in 11 dimensions.”

By

AlphaEvolve team, Google DeepMind

AI involvement

AlphaEvolve leverages an ensemble of state-of-the-art large language models: our fastest and most efficient model, Gemini Flash, maximizes the breadth of ideas explored, while our most powerful model, Gemini Pro, provides critical depth with insightful suggestions.

Model

AlphaEvolve (ensemble of Gemini Flash and Gemini Pro), as stated

Where

Google DeepMind blog

Checked

14 Oct 2026

Disproof claimed · 06 Oct 2026

A counterexample to Hadwiger's conjecture

“We disprove Hadwiger’s conjecture by constructing arbitrarily large graphs whose chromatic number exceeds their Hadwiger number. The examples have independence number at most two, and even their ordinary fractional chromatic number exceeds their Hadwiger number.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Formal proof

Lean 4, published by the source

Checked

14 Oct 2026

Partial result claimed · 04 Oct 2026

A Proof of the Linear Hadwiger Conjecture

“We show that there exists C ∈ ℕ such that K_t-minor free graphs are Ct-colorable.”

By

Sergey Norin, Raphael Steiner

AI involvement

The proof was found by GPT-6 Astra, following the directions by the authors. … The writing of this paper is due to the human authors.

Model

GPT-6 Astra, as stated

Where

arXiv

Formal proof

Lean 4, published by the source

Checked

14 Oct 2026

Partial result claimed · Revised · 06 Sep 2026

Beyond halfway to Hadwiger's conjecture

“Hadwiger conjectured in 1943 that every graph with no K_t minor has chromatic number at most t − 1. Delcourt and Postle proved that every graph with no K_t minor has chromatic number O(t log log t). We build on their result to improve this bound to O(t log log log t).”

By

Chun-Hung Liu, Jason Luo

AI involvement

ChatGPT Codex was used to help develop the proof. The authors supplied a high-level plan of attack and guided the development of the core argument.

Model

ChatGPT Codex, as stated

Where

arXiv

Checked

14 Oct 2026

Updates

• 09 Sep 2026 · Revised by Chun-Hung Liu, Jason Luo: “v2: significantly improve the bound and change the title”

Partial result claimed · 06 Oct 2026

An Upper Bound of 9/4 for the Matrix Multiplication Exponent

“We prove that the exponent of matrix multiplication over the complex numbers is at most 9/4.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Formal proof

Lean 4, published by the source

Checked

14 Oct 2026

Updates

• 07 Oct 2026 · Response · Scott Aaronson: “Matrix multiplication in n^(9/4+o(1)) time—a rational exponent for once (!), and via a completely different approach than was used for O(n^2.373) and so forth”
• 07 Oct 2026 · Response · Lance Fortnow: “Now these proofs haven't been fully verified but if they hold up, we've seen more progress in theoretical computer science in the last 24 hours than in the previous three decades combined!”

Partial result claimed · 17 Aug 2026

Improving the matrix multiplication exponent with modern optimization and AlphaEvolve

“Our combined approach yields an upper bound of ω < 2.371177, improving the previous best bound of 2.371339.”

By

Emilien Dupont, Marvin Eisenberger, Borislav Kozlovskii, Abbas Mehrabian, Francisco J. R. Ruiz, Abigail See, Renfei Zhou, Josh Alman, Virginia Vassilevska Williams, Matej Balog

AI involvement

Second, we leverage recent advances in machine learning to design a new optimization algorithm for this problem. Finally, we refine the resulting optimization algorithm with AlphaEvolve.

Model

AlphaEvolve, as stated

Where

arXiv

Checked

14 Oct 2026

Partial result claimed · 06 Oct 2026

Exact Birch–Swinnerton-Dyer Formula from Low Selmer Corank

“We prove the full Birch–Swinnerton-Dyer leading-term formula for every elliptic curve over ℚ whose full q-power Selmer group has corank zero or one at some prime q. The analytic and Mordell–Weil ranks equal that corank, and the Tate–Shafarevich group is finite.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Checked

14 Oct 2026

Updates

• 08 Oct 2026 · Response · Frank Calegari: “There are some results proving BSD under certain rank conditions. My first impression is that these are technical improvements on results already in the literature, and that they represent no genuine progress towards the higher-rank version of BSD.”

Partial result claimed · 06 Oct 2026

Generalized Star Height at Most Three

“Every regular language over a finite alphabet has generalized star height at most three, with complement taken in the same free monoid.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Formal proof

Lean 4, published by the source

Checked

14 Oct 2026

Partial result claimed · 06 Oct 2026

Generic Future Inextendibility with Square-Integrable Connection Near a Fixed Kerr Spacetime

“Strong cosmic censorship asks whether initial data determine a spacetime that cannot be continued beyond its maximal globally hyperbolic development. The regularity allowed for a continuation is part of the question. Kerr’s smooth inner horizon makes this distinction especially important [2]: a continuation can preserve the metric while losing the regularity needed to interpret its connection. Here we prove a local, Baire-category form of this assertion near each fixed rotating subextremal Kerr bridge, at the threshold of locally square-integrable connection coefficients.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Checked

14 Oct 2026

Partial result claimed · 06 Oct 2026

The Euclidean plane is not five-colorable

“We prove that every coloring of the Euclidean plane with five colors has a monochromatic unit-distance pair, with no regularity assumption on the color classes. Consequently, the chromatic number of the plane is either six or seven.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Formal proof

Lean 4, published by the source

Checked

14 Oct 2026

Updates

• 11 Oct 2026 · Response · Bill Gasarch: “OpenAI used the notion of weak measurable colorings to obtain a result about all colorings. That is new. This is a clear case of Searching has reached its limits; we need a new approach and OpenAI found one.”

Proof claimed · 06 Oct 2026

The Unique Games Theorem

“We prove the Unique Games Conjecture. For every fixed ε, δ ∈ (0, 1/2), we give a deterministic polynomial-time reduction from 3SAT to Unique Games over a fixed finite alphabet, with completeness at least 1 − ε and soundness at most δ.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Formal proof

Lean 4, published by the source

Checked

14 Oct 2026

Updates

• 07 Oct 2026 · Response · Lance Fortnow: “Now these proofs haven't been fully verified but if they hold up, we've seen more progress in theoretical computer science in the last 24 hours than in the previous three decades combined!”
• 07 Oct 2026 · Response · Scott Aaronson: “Or at least, we’re pretty sure that it’s a proof! There’s a Lean certificate, as there are for some of the other 372 breakthrough results (not all of them). But it also appears that no human has understood just about any of these proofs yet; the race to do so has just started.”

Proof claimed · 06 Oct 2026

Weak and strong normalization in pure type systems

“We prove that every weakly β-normalizing pure type system is strongly β-normalizing. Both properties quantify over all legal expressions in all valid contexts, and reduction acts inside type annotations. No functionality hypothesis is required. This resolves the β-Barendregt–Geuvers–Klop conjecture.”

By

OpenAI

AI involvement

This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.

Model

an unreleased internal OpenAI model, as stated

Where

openai/math repository

Formal proof

Lean 4, published by the source

Checked

14 Oct 2026

Proof claimed · Revised · 08 Sep 2026

On the Navier–Stokes Millennium Prize Problem

“Our system produced an analytical proof and a Lean formalization that an initially smooth fluid at rest can develop a singularity in a finite time. The fluid has a smooth force applied to it, and its energy remains finite through the entire dynamics, from rest to the formation of the singularity. This resolves the Navier–Stokes Millennium Prize problem by establishing statement “C” (and also “D”) in the official Millennium Prize formulation.”

By

OpenAI

AI involvement

We used a system of coordinating agents powered by our internal model. The agents had access to tools such as the ability to read from a cached version of the internet and the ability to run code. … The groups varied in size, and the group that produced the Navier–Stokes resolution involved on the order of 10,000 concurrent agents.

Model

an internal model that is significantly more capable than GPT-6 Astra, as stated

Where

OpenAI website (research post), with paper PDF and Lean repository

Formal proof

Lean 4, published by the source

Checked

14 Oct 2026

Updates

• 10 Sep 2026 · Revised by OpenAI: “Update — September 10, 2026: We have updated “Concurrent work” with findings from our investigation into whether user inputs could have influenced this result.”
• 11 Sep 2026 · Response · Clay Mathematics Institute: “Today, CMI shares in the excitement of the global mathematical community as we contemplate the announcement that the Navier-Stokes problem has apparently been settled. We hope to see waves of new human understanding unleashed as the innovations behind this work are analysed and interrogated. … The rules governing the prizes describe the process for evaluating what has been achieved and for assigning credit. The process is deliberately unhurried, but we will provide updates.”
• 12 Sep 2026 · Response · Silvia De Toffoli and Eamon Duede: “What OpenAI has given us is an answer. But it is not clear that they have delivered a fruitful solution. Perhaps, we will find that they have, but at the moment, the situation is far from clear.”
• 23 Sep 2026 · Response · Tapio Schneider: “The claimed result says that a fluid starting from rest, driven by just the right smooth stirring, develops an infinite velocity spike in finite time while its total kinetic energy remains bounded; the forcing is constructed to sustain the collapse. (The unforced version of the problem, whether smooth solutions exist for all time without external forcing, remains open.)”
• 28 Sep 2026 · Response · Zhen Lei and Xiao Ren: “This paper gives a readable and accessible version of the profile-construction part of OpenAI's manuscript "Finite Time Blowup for Navier-Stokes". We regard OpenAI's work as a major advance on the Navier-Stokes Millennium Prize Problem.”
• 04 Oct 2026 · Response · Diego Córdoba and Luis Martínez-Zoroa: “OpenAI’s September 8, 2026 announcement concerns two separate claims: blow-up for ordinary Navier–Stokes with smooth forcing, and blow-up for unforced Euler from smooth initial data. The first, if verified under the stated hypotheses, would establish an allowed breakdown alternative in the Millennium Problem formulation. It is distinct from unforced Navier–Stokes blow-up. At this moment we are not in a position to say anything substantive about a comparison between OpenAI’s constructions and our cascade methods.”
• 06 Oct 2026 · Response · Alexander Bastounis, Fabian Circelli and Anders C. Hansen: “To demonstrate the effect of this result we provide several examples of AI mistranslations of NL statements and proofs into Lean in practice, resulting in mismatches between NL proofs and their Lean `verifications'. These include OpenAI's announced Navier-Stokes proof. In particular, we show that the formalised Lean proof does not correspond to the NL proof of blow-up of solutions to the Navier-Stokes equations.”
• 09 Oct 2026 · Response · Thomas Hales: “The Navier-Stokes formalization has already been confirmed by more than a dozen proof-checkers. Cross-checking the proof by different kernels does not remove all doubt.”

Partial result claimed · Revised · 04 Sep 2026

A fixed-profile proof for prime gaps of at most 182

“Her August 2026 mixed-support preprint lowered the more-than-twelve-year-old bound H1 ≤ 246 to H1 ≤ 240; independent concurrent work by OpenAI, using her 2023 estimates, reached H1 ≤ 186, and the Axiom Math team further developed her framework to reach H1 ≤ 212. Building on these developments with additional Type II and Type III inputs and a new fixed profile, this paper proves H1 ≤ 182.”

By

Romyar Sharifi

AI involvement

The paper is credited to “GPT-6 Astra (OpenAI), prompted by Romyar Sharifi”.

Model

GPT-6 Astra (OpenAI), as stated

Where

Romyar Sharifi's UCLA web page

Checked

14 Oct 2026

Updates

• 11 Sep 2026 · Revised by Romyar Sharifi: “The 11 September 2026 version expanded citations and exposition; the stated results and numerical data were unchanged in that revision.”
• 18 Sep 2026 · Revised by Romyar Sharifi: “This edition incorporates corrections to the Type III result and adds its formal verification as a derivation from explicitly stated general published-theorem hypotheses.”
• 03 Oct 2026 · Revised by Romyar Sharifi: “Repository-publication references updated on 3 October 2026.”

Partial result claimed · 03 Sep 2026

A new bound for small gaps between primes

“Stadlmann recently proved that infinitely many pairs of distinct primes are apart by at most 240, improving upon the longstanding bound 246 established by Polymath8b. Building on her work, we prove that lim inf_{n→∞} (p_{n+1} − p_n) ≤ 212.”

By

François Charton, Letong Hong, Kenny Lau, Ken Ono, Guillaume Remy, Ho Chung Siu, Ashvin A. Swaminathan, Jesse Thorner, Yunzhou Xie (Axiom Math)

AI involvement

AxiomProver, an AI system under development by Axiom Math, autonomously generated from natural-language specifications a Lean certificate of the deduction of Theorem 1.1.

Model

AxiomProver, as stated

Where

Axiom Math website (paper PDF)

Checked

14 Oct 2026

Partial result claimed · 03 Sep 2026

Improved short gaps between primes

“We prove that lim inf_{n→∞} (p_{n+1} − p_n) ≤ 186, where p_n denotes the nth prime.”

By

OpenAI

AI involvement

The proof is due to GPT 6 Astra. … Astra helped establish a stronger bound of 186, showing that infinitely many pairs occur within this smaller distance.

Model

GPT 6 Astra, as stated

Where

OpenAI (paper PDF), with Lean repository openai/PrimeGaps186

Checked

14 Oct 2026

Partial result claimed · Revised · 02 Sep 2026

Fourteen and fifteen lonely runners

“We prove the Lonely Runner Conjecture for fourteen and fifteen runners.”

By

Jaan Allikvere

AI involvement

The author used large language models to assist with code development, drafting, exploring proof ideas, and searching for errors in the manuscript. No model output is treated as mathematical evidence.

Where

arXiv

Checked

14 Oct 2026

Updates

• 24 Sep 2026 · Revised by Jaan Allikvere: “v2: adds the fifteen-runner case and a sharper speed-product bound (logarithmic threshold about 415 instead of 810 for fifteen runners; 61 instead of 111 primes for fourteen); v1 covered fourteen runners only.”

Partial result claimed · 26 Apr 2026

Eleven, twelve, and thirteen lonely runners

“Ultimately, we provide a computer-assisted proof of the Lonely Runner Conjecture for k ∈ {10, 11, 12}.”

By

Touch Sungkawichai, Tanupat Trakulthongchai

AI involvement

The development of our code was assisted by AI-based tools, but the process was closely supervised and the code was manually verified.

Where

arXiv

Checked

14 Oct 2026

Partial result claimed · Revised · 27 Nov 2025

Nine and ten lonely runners

“Rosenfeld recently obtained a computer-assisted proof of the conjecture for 8 runners. By refining his approach with a sieve, we obtain proofs (also computer-assisted) for 9 and 10 runners.”

By

Tanupat Trakulthongchai

AI involvement

We employed OpenAI GPT-5 to assist with code generation, especially in low-level optimization.

Model

OpenAI GPT-5, as stated

Where

arXiv; published in The Electronic Journal of Combinatorics (2026, doi:10.37236/14972)

Checked

14 Oct 2026

Updates

• 18 Apr 2026 · Revised by Tanupat Trakulthongchai: “Updated theorem numbering to match with journal version; added references”