Prime Gaps at Most 186

This repository contains a Lean 4 formalization of a prime-gap bound and a Python numerical certificate. The Lean results remain conditional on three explicit input axioms ; the cited mathematical estimates and numerical computations have not been turned into Lean proofs of those inputs.

For the sequence of primes $p_n$ , the target bound is

The development derives $\mathrm{DHL}[40,2]$ from the inputs below: every admissible set of forty integer shifts has infinitely many translates containing at least two primes. Admissibility means omitting a residue class modulo every prime. Applying this to the included tuple of diameter 186 gives the gap bound.

The main declarations in PrimeGaps186.lean , in namespace PrimeGap186 , are:

For a prime $p$ , write $e_p(x)=\exp(2\pi i\widetilde{x}/p)$ , where $\widetilde{x}$ is any integer representative of $x\in\mathbb{F}_p$ . Define

The axiom PrimeGap186.kloosterman3_bound assumes the following bound for every prime $p$ and all $c\in\mathbb{F}_p^\times$ :