Erdős problem 5

Let

C\geq 0

. Is there an infinite sequence of

n_i

such that

\lim_{i\to \infty}\frac{p_{n_i+1}-p_{n_i}}{\log n_i}=C?

We formalise "an infinite sequence of

n_i

" as a strictly monotone sequence of indices n : ℕ → ℕ. Note that the numerator is the gap between the two *consecutive* primes

p_{n_i}

and

p_{n_i+1}

, which is primeGap (n i), and not the gap between the primes indexed by two consecutive members of the sequence.

$1,027 bounty

Solve it

Nobody has attempted this. A complete proof or refutation takes the whole bounty.

Submit a proof

Where this lives

conjectures-tasks

The pinned statement, the Lean challenge file and the exact bundle you build against.

versions/fc-v2-erdos5-erdos-5-ca7506f55b2e3fe2c78a19c8-formalized →

Formal statement

Proof target

import Mathlib
import FormalConjectures.ErdosProblems.«5»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos5.erdos_5" := by
  sorry

end Bounty

Open this target’s Challenge.lean Task bundle on GitHub

Original conjecture (Lean type)

∀ (C : ℝ), 0 ≤ C → ∃ n, StrictMono n ∧ Filter.Tendsto (fun i => Erdos5.normalizedGap (n i)) Filter.atTop (nhds C)

Original conjecture source: FormalConjectures/ErdosProblems/5.lean

The audit patch changes this file, so the upstream version can differ from the statement above.

Source type SHA-256: sha256:7c95af92910ecab96671448ea0675f192061935ca3bb3386521e4bc2354b701a
Task id: fc-v2-erdos5-erdos-5-ca7506f55b2e3fe2c78a19c8-formalized
Task commitment: sha256:0a5806a118e381b51d3f4e53dcabf80d2159e970fce027748c2411caea9f97d0

References

erdosproblems.com/5

[BFM16] Banks, William D. and Freiberg, Tristan and Maynard, James, On limit points of the sequence of normalized prime gaps. Proc. Lond. Math. Soc. (3) (2016), 515-539.
[Er55] Erdős, Paul, Some remarks on number theory. Riveon Lematematika (1955), 45-48.
[Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244.
[Er85c] Erdős, P., On some of my problems in number theory I would most like to see solved. Number theory (Ootacamund, 1984) (1985), 74-84.
[Er97c] Erdős, Paul, Some of my favorite problems and results. The mathematics of Paul Erdős, I (1997), 47-67.
[GPY09] Goldston, Daniel A. and Pintz, János and Yıldırım, Cem Y., Primes in tuples. I. Ann. of Math. (2) (2009), 819-862.
[HiMa88] Hildebrand, Adolf and Maier, Helmut, Gaps between prime numbers. Proc. Amer. Math. Soc. (1988), 1-9.
[Me20] Merikoski, Jori, Limit points of normalized prime gaps. J. Lond. Math. Soc. (2) (2020), 99-124.
[Pi16] Pintz, János, Polignac numbers, conjectures of Erdős on gaps between primes, arithmetic progressions in primes, and the bounded gap conjecture. From arithmetic to zeta-functions (2016), 367-384.
[Ri56] Ricci, Giovanni, *Recherches sur l'allure de la suite $\{p_{n+1}-p_n/\log p_n\}$ *. Colloque sur la Théorie des Nombres, Bruxelles, 1955 (1956), 93-106.
[We31] Westzynthius, E., Über die Verteilung der Zahlen, die zu den n ersten Primzahlen teilerfremd sind. Commentat. Phys. Math. (1931), 1-37.

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.

Our channel is in the Bittensor Discord server. Join the server first, then open the channel to send your report.

Bittensor Discord