Axiom Math

Axiom Math · Lean 4

Bounded gaps between primes: H1 ≤ 246

A unified formalization blueprint

A Lean 4 account of the proof that infinitely many consecutive prime gaps are at most 246. The argument combines Maynard’s multidimensional sieve with the parts of Polymath8b needed to reach the sharper bound.

The problem

Write pn for the nth prime. The quantity H1 = lim inf (pn+1 − pn) measures how close consecutive primes come infinitely often. Thus H1 ≤ 246 means that gaps of size at most 246 occur infinitely many times.

Maynard’s multidimensional sieve gave the bound 600. Polymath8b brought it down to 246 by enlarging the simplex in the variational problem and supplying an explicit finite certificate.

The formalization

The interactive blueprint breaks the argument into definitions, lemmas, and theorems. It shows what each result depends on and points to the corresponding Lean declaration.

PrimeGapsLib contains both sides of the proof: the general sieve theory and the explicit 50-dimensional certificate. The certificate is checked in Lean and combined with the theory in PrimeGaps.Bounded246, which proves that Bombieri–Vinogradov implies prime gaps bounded by 246 infinitely often.

Sources and scope

The proof draws on two papers. We formalize the Maynard argument in detail, but only the portion of Polymath8b used for the bound 246.

Core sieve Substantially formalized

James Maynard, Small gaps between primes

The multidimensional sieve, its first- and second-moment estimates, the variational quantity Mk, and the deduction of H1 ≤ 600.

Published paper arXiv

246 refinement Scoped extract

D. H. J. Polymath, Variants of the Selberg sieve

We use the enlarged-simplex refinement of Theorem 3.12(i), the certificate argument from Theorem 3.13(i) and §6.2, and the 50-tuple endgame. The other results in Polymath8b are not part of this project.

Published paper arXiv

How the formalization was built

We first wrote the proof as a blueprint, with a separate entry for each definition and lemma. The dependency graph then gave us an order in which to formalize it.

  1. Create the blueprint

    Give every definition, lemma, and theorem a label, a precise statement, and a list of the earlier results it uses.

  2. Layer the dependency graph

    Arrange the graph in layers. By the time we reach a node, all of its dependencies have already been formalized.

  3. Formalize with AxiomProver

    AxiomProver is Axiom Math’s AI system for mathematical research through formal proof. We gave it one layer at a time, together with the completed dependencies. It produced machine-checkable Lean 4 proofs built on Mathlib.

How the proof fits together

1
Maynard sieveBuild and evaluate the weighted sums S₁ and S₂.
2
Enlarged simplexUse the Polymath8b variational refinement at k = 50.
3
Certificate and tupleCombine M50,1/25 > 4.0043 with an admissible tuple of diameter 246.
4
H1 ≤ 246Infinitely many consecutive prime gaps have size at most 246.

Explore the project

PrimeGapsLib

The public Lean library, including the theory and the 246 certificate.

Zulip discussion Forthcoming

The project discussion link will be added when its Zulip topic opens.

Contributors

Mathematical contributors Engineering contributors