Bounded gaps between primes

zhang_bounded_prime_gaps — a formalization challenge from the lean-eval benchmark.

Notes

Zhang's bounded-gaps theorem, sharpened by Maynard and the Polymath8 project: for every n there exist primes p < q with n ≤ p and q - p ≤ 246, the post-Polymath bound recorded by Knill. Equivalently, infinitely many prime pairs differ by at most 246. mathlib has Nat.Prime and prime-counting estimates, but no Selberg/GPY sieve.

Formal statement

/-- **Bounded gaps between primes.** For every `n` there is a pair of primes
`p < q` with `n ≤ p` and `q - p ≤ 246`. -/
theorem zhang_bounded_prime_gaps :
    ∀ n : ℕ, ∃ p q : ℕ, n ≤ p ∧ p.Prime ∧ q.Prime ∧ p < q ∧ q - p ≤ 246 := by
  sorry

Informal solution sketch

Use the GPY/Maynard multidimensional sieve. Choose an admissible k-tuple of linear forms and a sieve weight optimizing a ratio of two quadratic forms in a smooth cutoff; Maynard's variational argument shows that for k large enough the weighted count guarantees at least two primes among the shifted forms in infinitely many translates. The Polymath8 optimization of the cutoff and the choice of an admissible 50-tuple yields the explicit gap bound 246.

Source

Y. Zhang, Bounded gaps between primes, Ann. of Math. 179 (2014), 1121-1174; J. Maynard, Small gaps between primes, Ann. of Math. 181 (2015), 383-413; D. H. J. Polymath, Variants of the Selberg sieve, and bounded intervals containing many primes, Res. Math. Sci. 1 (2014), Art. 12. Listed as §224 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Knill, §224.

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: zhang_bounded_prime_gaps
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.