Make the 246 bounded-prime-gap theorem unconditional

Challenge/Basic.lean

@@ -8,6 +8,8 @@ module
 public import Mathlib.Analysis.SpecialFunctions.Pow.Real
 public import Mathlib.NumberTheory.PrimeCounting
 
+set_option autoImplicit false
+
 /-! # The statement file
 
 This file is built by humans to act as the standard to check the main theorems against, using

ChallengeFast/Basic.lean

@@ -8,6 +8,8 @@ module
 public import Mathlib.Analysis.SpecialFunctions.Pow.Real
 public import Mathlib.NumberTheory.PrimeCounting
 
+set_option autoImplicit false
+
 /-! # The faster statement file
 
 This file is built by humans to act as the standard to check the main theorems against, using

PrimeGaps.lean

@@ -1,3 +1 @@
-module  -- shake: keep-all --deprecated_module: ignore
-
-public import PrimeGaps.Bounded246
+import PrimeGaps.Unconditional246

PrimeGaps/Unconditional246.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2026 Axiom Math. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Axiom Math, Jonas Whidden
+-/
+
+import BombieriVinogradov.Assembly.PrimeCountingConversion.Main
+import PrimeGaps.Bounded246
+
+/-! # Unconditional Prime Gaps Bounded by 246
+
+This file combines the formalized Bombieri--Vinogradov theorem with the
+conditional bounded-gap result to remove the final analytic hypothesis.
+-/
+
+set_option autoImplicit false
+
+/-- The Bombieri--Vinogradov theorem in the exact form consumed by PrimeGapsLib. -/
+theorem bombieriVinogradov : BombieriVinogradov :=
+  BombieriVinogradov.PrimeCountingConversion.weighted_to_prime_counting
+
+/-- Infinitely many consecutive prime gaps are at most 246. -/
+theorem frequently_prime_gap_le_246 :
+    ∃ᶠ m in Filter.atTop, Nat.nth Nat.Prime (m + 1) - Nat.nth Nat.Prime m ≤ 246 :=
+  bombieriVinogradov_implies_frequently_prime_gap_le_246 bombieriVinogradov
+
+/-- Above every threshold there are two primes at distance at most 246. -/
+theorem prime_gap_le_246 :
+    ∀ n₀ : ℕ, ∃ p q : ℕ, n₀ ≤ p ∧ p < q ∧ p.Prime ∧ q.Prime ∧ q ≤ p + 246 :=
+  bombieriVinogradov_implies_prime_gap_le_246 bombieriVinogradov
+
+/-- Arbitrarily far out, two successive entries in the prime enumeration differ by at most 246. -/
+theorem nth_prime_gap_le_246 :
+    ∀ n₀ : ℕ, ∃ n ≥ n₀, (n + 1).nth Nat.Prime ≤ n.nth Nat.Prime + 246 :=
+  bombieriVinogradov_implies_nth_prime_gap_le_246 bombieriVinogradov

PrimeGapsCert/Gap246/RHS/WeightBridge.lean

@@ -111,6 +111,9 @@ theorem certRhsWeightLocations_bound (hchecks : CertRhsFeatureKeyChecks) :
       (by simpa only [certRhsDegreeBound] using hexponent)
   simpa only using hactive
 
+-- These generated-scale declarations are kernel-checked by the build, but the
+-- `checkType` linter deterministically exhausts its heartbeat budget on them.
+@[nolint checkType]
 private theorem certRhsRawLocation (hchecks : CertRhsFeatureKeyChecks) (label : Fin 1295)
     (exponent : Fin 26)
     (hexponent : exponent.val ∈ insert 0 (certSig (certLabelSignature label)).toFinset) :
@@ -128,6 +131,7 @@ private theorem certRhsRawLocation (hchecks : CertRhsFeatureKeyChecks) (label :
       using hbound
 
 set_option exponentiation.threshold 1000 in
+@[nolint checkType]
 private theorem certRhsRawTransitionWeight (label : Fin 1295) (exponent : ℕ)
     (hexponent : exponent ∈ insert 0 (certSig (certLabelSignature label)).toFinset) :
     (if certRhsSign label = 0 then (certRhsMagnitude label exponent : ℤ)
@@ -171,6 +175,7 @@ private theorem certRhsRawTransitionWeight (label : Fin 1295) (exponent : ℕ)
     push_cast
     ring
 
+@[nolint checkType]
 private theorem certRhsExponentSum (hchecks : CertRhsFeatureKeyChecks)
     (label : Fin 1295) (feature : Fin 1504) :
     (∑ exponent ∈ Finset.range 26,

PrimeGapsTheory/NumberTheory/BombieriVinogradov.lean

@@ -5,14 +5,15 @@ Authors: Axiom Math
 -/
 module
 
+public import BombieriVinogradov.Definitions.Statement
 public import PrimeGapsTheory.NumberTheory.LevelOfDistribution
 
 import PrimeGapsTheory.Tactic.PaperTag
 
 /-! # The Bombieri-Vinogradov theorem
 
-The Bombieri-Vinogradov theorem, packaged as a proposition that is carried as a hypothesis
-throughout the development, together with its standard reformulations.
+The exact Bombieri-Vinogradov statement, shared with its complete formalization,
+together with the standard conditional reformulations used by the prime-gaps development.
 
 ## Main definitions
 
@@ -29,16 +30,6 @@ throughout the development, together with its standard reformulations.
 
 open Nat Real Finset Filter Asymptotics
 
-/-- The **Bombieri-Vinogradov Theorem**, as a proposition.
-
-`ℕ` has level of distribution `θ` for all `θ < 1 / 2`.
-
-This will be a hypothesis throughout.
--/
-def BombieriVinogradov : Prop :=
-  ∀ θ < (1 / 2 : ℝ), ∀ A ≥ (1 : ℝ), ∃ c > (0 : ℝ), ∀ x ≥ (3 : ℝ),
-    ∑ q ∈ Icc (1 : ℕ) ⌊x ^ θ⌋₊, ⨆ a : (ZMod q)ˣ, |(π(x; q, a) - π(x) / φ q : ℝ)| ≤ c * x / x.log ^ A
-
 theorem BombieriVinogradov.hasLevelOfDistribution (hBV : BombieriVinogradov)
     {θ : ℝ} (hθ : θ < 1 / 2) : HasLevelOfDistribution Set.univ θ 1 := by
   simpa [HasLevelOfDistribution] using hBV _ hθ

PrimeGapsTheory/NumberTheory/PrimeCountingZMod.lean

@@ -6,7 +6,7 @@ Authors: Axiom Math
 module
 
 
-public import PrimeNumberTheoremAnd.Defs
+public import BombieriVinogradov.Definitions.PrimeCounting
 
 /-!
 # The Prime Counting Function in Arithmetic Progressions
@@ -205,10 +205,6 @@ section PrimeCountingZMod
 
 namespace Real
 
-/-- The number of primes at most `x` in the residue class `a` modulo `q`. -/
-public noncomputable def primeCountingZMod (x : ℝ) (q : ℕ) (a : ZMod q) : ℕ :=
-  {p : ℕ | p.Prime ∧ (p : ZMod q) = a ∧ p ≤ x}.ncard
-
 /-- Write `π(x; q, a)` for `Real.primeCountingZMod x q a`. -/
 scoped[Real] notation "π(" x "; " q ", " a ")" => Real.primeCountingZMod x q a
 

README.md

@@ -6,7 +6,10 @@ Public Lean library for formalizations related to prime gaps, maintained by Axio
 
 ## Dependencies
 
-This repository depends on [an internal fork of PrimeNumberTheoremAnd](https://github.com/AxiomMath/PrimeNumberTheoremAnd) (original [here](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd)), changed to use the module system.
+The Lean 4.33.1 build depends on a
+[module-compatible PrimeNumberTheoremAnd fork](https://github.com/kimihiro64/PrimeNumberTheoremAnd/commit/0f15a38c619298b5cd786d39a84dd4bb8997324c)
+(based on the [original project](https://github.com/AlexKontorovich/PrimeNumberTheoremAnd)) and on the
+[formalization of the Bombieri--Vinogradov theorem](https://github.com/kimihiro64/bombieri-vinogradov/commit/afbcbb5959ad22f86ede6b3a53d5d396142fd32b).
 
 ## Structure
 
@@ -16,23 +19,25 @@ This repository depends on [an internal fork of PrimeNumberTheoremAnd](https://g
 
 ## Main Results
 
-1. The Bombieri–Vinogradov theorem implies prime gaps bounded by 246 infinitely often, located in [PrimeGaps.Bounded246](PrimeGaps/Bounded246.lean).
-2. The Bombieri–Vinogradov theorem implies prime gaps bounded by 600 infinitely often, located in [PrimeGapsTheory.Endgame.Main](PrimeGapsTheory/Endgame/Main.lean).
-3. The Bombieri–Vinogradov theorem and existence of certificate imply prime gaps bounded by 246 infinitely often, located in [PrimeGapsTheory.Gap246.Endgame.Main](PrimeGapsTheory/Gap246/Endgame/Main.lean).
+1. Unconditionally, prime gaps are at most 246 infinitely often, located in [PrimeGaps.Unconditional246](PrimeGaps/Unconditional246.lean).
+2. The exact Bombieri--Vinogradov theorem consumed by the bounded-gap proof is exposed as `bombieriVinogradov` in [PrimeGaps.Unconditional246](PrimeGaps/Unconditional246.lean).
+3. The original conditional 246 result remains in [PrimeGaps.Bounded246](PrimeGaps/Bounded246.lean).
+4. The Bombieri--Vinogradov theorem implies prime gaps bounded by 600 infinitely often, located in [PrimeGapsTheory.Endgame.Main](PrimeGapsTheory/Endgame/Main.lean).
+5. The Bombieri--Vinogradov theorem and existence of the numerical certificate imply prime gaps bounded by 246 infinitely often, located in [PrimeGapsTheory.Gap246.Endgame.Main](PrimeGapsTheory/Gap246/Endgame/Main.lean).
 
-Formal versions of these statements can be found in the formal challenge described in [§Comparator](#comparator).
+Formal challenge files for the original conditional components are described in [§Comparator](#comparator).
 
 ## Comparator
 
-A formal challenge that is self-contained and only depends on Mathlib is located in [Comparator.Challenge](Comparator/Challenge.lean). It contains statement 1 of [§Main Results](#main-results) with `sorry` as proof.
+A formal challenge that is self-contained and only depends on Mathlib is located in [Comparator.Challenge](Comparator/Challenge.lean). It contains the conditional 246-gap theorem with `sorry` as proof. The imported Bombieri--Vinogradov formalization has its own separately checked Palomar Challenge/Solution boundary; [PrimeGaps.Unconditional246](PrimeGaps/Unconditional246.lean) composes that theorem with this repository's conditional result.
 
 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`. Then, run the following command:
 ```
 lake env comparator Comparator/comparator.json
 ```
 Beware that this can take hours.
 
-The proofs of statements 2 and 3 of [§Main Results](#main-results) compile much faster, so we also included a formal challenge for them in [Comparator.ChallengeFast](Comparator/ChallengeFast.lean). To verify this repository against this challenge file, run the following command:
+The conditional 600-gap and certificate-to-246 proofs compile much faster, so we also included a formal challenge for them in [Comparator.ChallengeFast](Comparator/ChallengeFast.lean). To verify this repository against this challenge file, run the following command:
 ```
 lake env comparator Comparator/comparator_fast.json
 ```

Solution/Basic.lean

@@ -1,3 +1,5 @@
 module
 
 import PrimeGaps.Bounded246
+
+set_option autoImplicit false

SolutionFast/Basic.lean

@@ -2,3 +2,5 @@ module
 
 import PrimeGapsTheory.Endgame.Main
 import PrimeGapsTheory.Gap246.Endgame.Main
+
+set_option autoImplicit false

formalization.yaml

@@ -4,12 +4,13 @@ version: "v0.4"
 
 project:
   name: "PrimeGapsLib"
-  authors: [Evan Chen, Sidharth Hariharan, Kenny Lau, Bhavik Mehta, Ken Ono, Ashvin Swaminathan, Jesse Thorner, Yunzhou Xie]
+  authors: [Evan Chen, Sidharth Hariharan, Kenny Lau, Bhavik Mehta, Ken Ono, Ashvin Swaminathan, Jesse Thorner, Yunzhou Xie, Jonas Whidden]
   description: >
     `PrimeGapsLib` is an evolving codebase aimed at housing results about gaps in primes. The
-    flagship result thus far is that pairs of primes are separated by at most 246 infinitely often,
-    conditional on the Bombieri-Vinogradov theorem. The 246 proof was generated collaboratively
-    between human formalisers at Axiom Math and AxiomProver, their in-house theorem proving system.
+    flagship result is that pairs of primes are separated by at most 246 infinitely often. The
+    bounded-gap implication and numerical certificate were generated collaboratively between human
+    formalisers at Axiom Math and AxiomProver, their in-house theorem proving system. A separately
+    formalized Bombieri-Vinogradov theorem now discharges the implication's analytic hypothesis.
     Community feedback and contributions are welcome!
   responsible_maintainers: [Kenny Lau, Ashvin Swaminathan]
   license: "Apache-2.0"
@@ -30,39 +31,54 @@ sources:
     relationship: "background"
     note: "Along the way to the 246 result, we also formalise the fact that the Bombieri-Vinogradov theorem implies Maynard's 600 bound. However, this is not the primary result of this repository, and is mentioned here purely for completeness."
 
+related_formalizations:
+  - id: "https://github.com/kimihiro64/bombieri-vinogradov/commit/afbcbb5959ad22f86ede6b3a53d5d396142fd32b"
+    relationship: "builds-on"
+    note: "Proves the exact Bombieri-Vinogradov statement consumed by this repository."
+  - id: "https://github.com/kimihiro64/PrimeNumberTheoremAnd/commit/0f15a38c619298b5cd786d39a84dd4bb8997324c"
+    relationship: "builds-on"
+    note: "Lean 4.33.1 module-compatible PNT infrastructure used by both formalizations."
+
 classification:
   arxiv: [math.NT]
   msc2020: [11N05, 11N35, 11N36, 11P32]  # Based on the MSC classifications of the sources
 
 status:
-  scope: "Developing a consolidated Lean library for results on gaps between primes, the flagship result being that the Bombieri-Vinogradov theorem implies that that there are infinitely many pairs of primes separated by no more than 246."
+  scope: "A consolidated Lean library proving unconditionally that there are infinitely many pairs of primes separated by no more than 246, by composing the certified conditional bounded-gap argument with a formal proof of the Bombieri-Vinogradov theorem."
   sorry_count: 0
   sorry_in_definitions: 0
   axioms: [propext, Classical.choice, Quot.sound]
   main_results:
-  - declaration: "bombieriVinogradov_implies_prime_gap_le_246"
-    file: "PrimeGaps/Bounded246.lean"
+  - declaration: "prime_gap_le_246"
+    file: "PrimeGaps/Unconditional246.lean"
+    sorry_count: 0
+    axioms: [propext, Classical.choice, Quot.sound]
+    literature_dependencies:
+    - statement: "The Bombieri-Vinogradov theorem and the Polymath8b bounded-gap implication"
+      source: "Bombieri-Vinogradov in Lean; Variants of the Selberg sieve, Theorem 4(i)"
+  - declaration: "nth_prime_gap_le_246"
+    file: "PrimeGaps/Unconditional246.lean"
     sorry_count: 0
     axioms: [propext, Classical.choice, Quot.sound]
-    comparator_config: "Comparator/comparator.json"
     literature_dependencies:
-    - statement: "The Bombieri-Vinogradov Theorem"
-      source: "Small gaps between primes (p.384)"
-  - declaration: "bombieriVinogradov_implies_nth_prime_gap_le_246"
-    file: "PrimeGaps/Bounded246.lean"
+    - statement: "The Bombieri-Vinogradov theorem and the Polymath8b bounded-gap implication"
+      source: "Bombieri-Vinogradov in Lean; Variants of the Selberg sieve, Theorem 4(i)"
+  - declaration: "bombieriVinogradov"
+    file: "PrimeGaps/Unconditional246.lean"
     sorry_count: 0
     axioms: [propext, Classical.choice, Quot.sound]
-    comparator_config: "Comparator/comparator.json"
     literature_dependencies:
-    - statement: "The Bombieri-Vinogradov Theorem"
-      source: "Small gaps between primes (p.384)"
+    - statement: "The Bombieri-Vinogradov theorem"
+      source: "Bombieri-Vinogradov in Lean"
 
 automation:
   methods:
     - method: "autonomous"
       models: [AxiomProver]
+    - method: "agent"
+      models: [OpenAI Codex, GPT-5 series]
     - method: "manual"
-  notes: "Foundational definitions formalised manually, some definitions formalised autonomously, most theorems formalised autonomously"
+  notes: "Foundational definitions were formalised manually; much of the bounded-gap development used AxiomProver; the unconditional integration and its Bombieri-Vinogradov dependency used OpenAI Codex under human direction."
 
 review:
   status: "self-assessed"
@@ -74,19 +90,31 @@ review:
     development of this formalisation took place in a repository internal to Axiom Math.
     Pull requests to that repository were not typically merged without thorough vetting from the
     reviewers. Before the contents of the internal repository were moved to this public repository,
-    there were more rounds of code review for both quality and fidelity.
+    there were more rounds of code review for both quality and fidelity. The unconditional
+    Bombieri-Vinogradov integration is currently self-assessed and has not yet received independent
+    expert review.
 
 alignment:
   statements:
     - source: "Variants of the Selberg sieve (Theorem 4(i))"
-      lean: "bombieriVinogradov_implies_prime_gap_le_246"
-      module: "PrimeGaps.Bounded246"
-      status: "Proved, conditional on the Bombieri-Vinogradov theorem"
-      note: "The primary result of this repository."
+      lean: "prime_gap_le_246"
+      module: "PrimeGaps.Unconditional246"
+      status: "Proved unconditionally"
+      note: "The conditional Polymath8b implication is composed with the formalized Bombieri-Vinogradov theorem."
+    - source: "Variants of the Selberg sieve (Theorem 4(i))"
+      lean: "nth_prime_gap_le_246"
+      module: "PrimeGaps.Unconditional246"
+      status: "Proved unconditionally"
+      note: "Equivalent formulation in terms of the enumerated sequence of primes."
+    - source: "Bombieri-Vinogradov theorem in the Maynard level-of-distribution formulation"
+      lean: "bombieriVinogradov"
+      module: "PrimeGaps.Unconditional246"
+      status: "Proved"
+      note: "Imported from the pinned Bombieri-Vinogradov formalization and matched to PrimeGapsLib's exact consumer type."
     - source: "Small gaps between primes (Theorem 1.4, second inequality)"
       lean: "bombieriVinogradov_implies_prime_gap_le_600"
       module: "PrimeGapsTheory.Endgame.Main"
       status: "Proved, conditional on the Bombieri-Vinogradov theorem"
       note: "We proved Maynard's 600 bound along the way to proving Polymath8b's 246 bound."
 
-acknowledgements: "We acknowledge the dependence of our repository on Alex Kontorovich and Terence Tao's `PrimeNumberTheoremAnd` project."
+acknowledgements: "We acknowledge the dependence of this repository on Alex Kontorovich and Terence Tao's `PrimeNumberTheoremAnd` project and on the cited Bombieri-Vinogradov formalization."