Summary
formalization.yaml attributes the formalized 600 bound to Maynard's Theorem 1.4, second inequality, in two places:
sources[1].location: "Theorem 1.4, second inequality"
alignment.statements[].source: "Small gaps between primes (Theorem 1.4, second inequality)" (for bombieriVinogradov_implies_prime_gap_le_600)
That attribution does not match the formal statement — in either hypothesis or conclusion.
What the paper actually says
James Maynard, Small gaps between primes, Annals of Math. 181(1):383–413 (2015) (arXiv:1311.4600v3):
Theorem 1.3. We have $\liminf_n (p_{n+1} - p_n) \le 600$.
... The proof is essentially elementary, relying only on the Bombieri-Vinogradov theorem.
Theorem 1.4. Assume that the primes have level of distribution θ for every θ < 1. Then
$\liminf_n (p_{n+1} - p_n) \le 12$, $\quad \liminf_n (p_{n+2} - p_n) \le 600$.
Why the current entry is wrong for this repository
PrimeGapsTheory.Endgame.Main.thm_main (bombieriVinogradov_implies_prime_gap_le_600) assumes exactly BombieriVinogradov and concludes a bound on consecutive gaps {n+1} - p_n$. That is:
- Theorem 1.3 — BV hypothesis ✓, consecutive-gap conclusion ✓
- Not Theorem 1.4's second inequality — that one needs the much stronger level-of-distribution-θ<1 hypothesis and concludes {n+2} - p_n$ instead.
Note the proof implemented in the repository also follows Theorem 1.3's route verbatim: {105} > 4$, $\theta = 1/4 + 1/M_{105}$, giving $\theta M_{105}/2 > 1$ with $\theta < 1/2$ from Bombieri–Vinogradov.
Suggested fix
Replace both occurrences with "Theorem 1.3". PR incoming.
Summary
formalization.yamlattributes the formalized 600 bound to Maynard's Theorem 1.4, second inequality, in two places:sources[1].location: "Theorem 1.4, second inequality"alignment.statements[].source: "Small gaps between primes (Theorem 1.4, second inequality)"(forbombieriVinogradov_implies_prime_gap_le_600)That attribution does not match the formal statement — in either hypothesis or conclusion.
What the paper actually says
James Maynard, Small gaps between primes, Annals of Math. 181(1):383–413 (2015) (arXiv:1311.4600v3):
Why the current entry is wrong for this repository
PrimeGapsTheory.Endgame.Main.thm_main(bombieriVinogradov_implies_prime_gap_le_600) assumes exactlyBombieriVinogradovand concludes a bound on consecutive gaps {n+1} - p_n$. That is:Note the proof implemented in the repository also follows Theorem 1.3's route verbatim: {105} > 4$,$\theta = 1/4 + 1/M_{105}$ , giving $\theta M_{105}/2 > 1$ with $\theta < 1/2$ from Bombieri–Vinogradov.
Suggested fix
Replace both occurrences with "Theorem 1.3". PR incoming.