AxiomProver Formalizes the BGP246 Bounded Prime-Gap Theorem in Lean
Carina Hong and Axiom Math announce an AxiomProver-produced Lean 4 formalization of the BGP246 theorem that prime gaps of at most 246 occur infinitely often; the public repository separates theory and numerical certificates and formalizes the existing best-known bound rather than improving it.
On August 18, 2026, Carina Hong announced what she described as AxiomProver's first large-scale Lean formalization: the BGP246 theorem on bounded gaps between primes. Axiom Math's accompanying announcement calls the result a machine-checkable formalization of the best-known bound on recurring small prime gaps.
The public Lean library states that the Bombieri-Vinogradov theorem implies that gaps of at most 246 occur infinitely often. It separates the mathematical theory from large numerical certificate computations and provides comparator challenges for checking the main theorem against a self-contained statement. This formalizes an existing theorem rather than improving the bound toward the twin-prime conjecture.
The announcement attributes the formalization to AxiomProver, and the repository is implemented in Lean 4. The public materials do not name individual members responsible for the formalization, so this item records Hong as the reporter and AxiomProver as the system attribution.