Public Lean library for formalizations related to prime gaps, maintained by Axiom Math.
This repository depends on an internal fork of PrimeNumberTheoremAnd (original here), changed to use the module system.
- PrimeGaps: the main library combining PrimeGapsTheory and PrimeGapsCert.
- PrimeGapsTheory: the main formalization excluding large numerical computations, which builds quickly.
- PrimeGapsCert: large numerical computations that might take a long time to build.
- The Bombieri–Vinogradov theorem implies prime gaps bounded by 246 infinitely often, located in PrimeGaps.Bounded246.
- The Bombieri–Vinogradov theorem implies prime gaps bounded by 600 infinitely often, located in PrimeGapsTheory.Endgame.Main.
- The Bombieri–Vinogradov theorem and existence of certificate imply prime gaps bounded by 246 infinitely often, located in PrimeGapsTheory.Gap246.Endgame.Main.
Formal versions of these statements can be found in the formal challenge described in §Comparator.
A formal challenge that is self-contained and only depends on Mathlib is located in Comparator.Challenge. It contains formal statements of §Main Results with sorry as proof.
This repository can be verified against the formal challenge with the Lean comparator on a Linux machine. First, follow the instructions in https://github.com/leanprover/comparator to install comparator.
For the version that builds faster, which only includes 2 and 3 from §Main Results, run the following command:
lake env comparator Comparator/comparator.json
This skips the numerical certificate which can take a long time.
For the full version, which includes 1, 2, and 3 from §Main Results, run the following command:
lake env comparator Comparator/comparator_full.json
This includes the numerical certificate which can take a long time.