Axiom Math translated a proof into machine-checkable code: infinitely many consecutive primes differ by no more than 246

Axiom Math translated a proof into machine-checkable code: infinitely many consecutive primes differ by no more than 246

On August 17, IEEE Spectrum reported that the Axiom Math team had published a formalization of this bound. The program verifies the proof according to the rules of logic. AxiomProver generated Lean 4 code, which project contributors reviewed and compiled into the PrimeGapsLib library. Its modules can be reused in later formal proofs.

The twin prime conjecture asks whether infinitely many pairs of primes differ by two. This question remains open. In 2013, mathematician Yitang Zhang proved that the gap between infinitely many pairs of consecutive primes could be bounded by 70 million. James Maynard reduced the upper bound to 600, and the collaborative Polymath8b project reduced it further to 246. Axiom formalized this specific bound on the project website.

A conventional proof is presented through the text and calculations in a paper. The Axiom team first produced a detailed map of the definitions, lemmas, and dependencies between them. AxiomProver then generated Lean 4 proofs for these formal goals. Lean 4 is a language in which a proof is written as a program, and a proof checker verifies every step against the rules of logic. Project contributors subsequently reviewed the code and organized it into a library.

In the PrimeGapsLib repository, the general theory is separated from the numerical certificate, which consists of the computations that establish the bound of 246. A later formalization can import a completed lemma as a dependency, and Lean will verify that the conditions for applying it are satisfied.

Verified components of one proof can now serve as dependencies in another.