A new bound for small gaps between primes:
Write . Stadlmann had recently proved , improving the bound of Polymath8b. Building on her work, this paper proves : infinitely many pairs of consecutive primes are at most apart.
- Result
- Proved(see note)
- Status
- Partial result
- AI contribution
- AI-assisted
- Method
- Argument
- Field
- Analytic number theory
- Posed by
- Alphonse de Polignac (the twin prime conjecture); the bounded form since Goldston, Pintz and Yıldırım
- Year posed
- 1849
- Years open
- 177y
- Solved
- 2026-09-03
- Model
- AxiomProver
- Vendor
- Axiom Math
- Collaborators
- François Charton, Letong Hong, Kenny Lau, Ken Ono, Guillaume Remy, Ho Chung Siu, Ashvin A. Swaminathan, Jesse Thorner, Yunzhou Xie
- Verification
- Lean-checked, statement unaudited
- Publication
- Preprint
- Significance
- 62 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
, improving Stadlmann's of three days earlier and the of Polymath8b that had stood since 2014. The twin prime conjecture, , is untouched. Held the record for hours at most: OpenAI's paper claiming is dated 30 August, four days before this one, though its Lean development appeared on 2 September.
What the AI did
The mathematics is the authors'. The AI contribution is the formal certificate, and the paper is precise about it in Appendix A: "AxiomProver, an AI system under development by AxiomMath, autonomously generated from natural-language specifications a Lean certificate of the deduction of Theorem 1.1." The certificate takes as hypotheses the five Type I, Type II and Type III equidistribution estimates of Section 5, the bilinear Bombieri-Vinogradov theorem below the half-level, the Harman decomposition, and the variational certificate. Nothing in the paper claims the model found the argument, and the abstract does not mention AI at all.
The same group's AxiomProver had formalised the twelve-year-old 246 bound in Lean a few weeks earlier, which is the work this builds its tooling on.
Verification
A preprint one day old, not peer reviewed. Its Lean certificate was produced by AxiomProver and is conditional on the equidistribution estimates and the Bombieri-Vinogradov theorem stated in the paper, so it certifies the deduction rather than the analytic inputs. Nine authors, several of whom work on exactly this, take responsibility for the mathematics. No independent expert has read it on the record, and this site has not rebuilt the certificate.