Erdős problem 6
There are infinitely many such that , where denotes the prime gap function.
Sources
FormalConjectures/ErdosProblems/
6.lean
Retained formal statement
For all , there are infinitely many such that , where denotes the prime gap function.
Proved by Banks, Freiberg, and Turnage-Butterbaugh [BFT15] with an application of the Maynard-Tao machinery concerning bounded gaps between primes [Ma15]
∀ (m : ℕ), {n | ∀ i ∈ Finset.range m, primeGap (n + i) < primeGap (n + i + 1)}.InfiniteSolvedStatement only, no proof