Erdős Problem 375

References:

• erdosproblems.com/375
• [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).
• [RST75] Ramachandra, K. and Shorey, T. N. and Tijdeman, R., On Grimm's problem relating to factorisation of a block of consecutive integers. J. Reine Angew. Math. (1975), 109-124.

def Erdos375.Erdos375Prop : Prop

This is a proposition saying that for any n ≥ 1 and any k, if n + 1, ..., n + k are all composite, then there are distinct primes p₁, ... pₖ such that pᵢ ∣ n + i for all 1 ≤ i ≤ k.

Equations

• Erdos375.Erdos375Prop = ∀ n ≥ 1, ∀ (k : ℕ), (∀ i < k, ¬Nat.Prime (n + i + 1)) → ∃ (p : Fin k → ℕ), Function.Injective p ∧ ∀ (i : Fin k), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1

theorem Erdos375.erdos_375 : True ↔ Erdos375Prop

Is Erdos375Prop true?

theorem Erdos375.erdos_375.variants.bounded_gap : Erdos375Prop → ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Nat.nth Nat.Prime (n + 1)) - ↑(Nat.nth Nat.Prime n) < ↑(Nat.nth Nat.Prime n) ^ (1 / 2 - c)

If Erdos375Prop is true, then (n + 1).nth Prime - n.nth Prime < (n.nth Prime) ^ (1 / 2 - c) for some c > 0.

theorem Erdos375.erdos_375.variants.legendre : Erdos375Prop → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ p ∈ Set.Ioo (n ^ 2) ((n + 1) ^ 2), Nat.Prime p

In particular, if Erdos375Prop is true, then Legendre's conjecture is asymptotically true.

theorem Erdos375.erdos_375.variants.le_two (n : ℕ) : n ≥ 1 → ∀ k ≤ 2, (∀ i < k, ¬Nat.Prime (n + i + 1)) → ∃ (p : Fin k → ℕ), Function.Injective p ∧ ∀ (i : Fin k), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1

It is easy to see that for any n ≥ 1 and k ≤ 2, if n + 1, ..., n + k are all composite, then there are distinct primes p₁, ... pₖ such that pᵢ ∣ n + i for all 1 ≤ i ≤ k.

theorem Erdos375.erdos_375.variants.log : ∃ c > 0, ∀ (n k : ℕ), ↑k < c * (Real.log ↑n / Real.log (Real.log ↑n)) ^ 3 → (∀ i < k, ¬Nat.Prime (n + i + 1)) → ∃ (p : Fin k → ℕ), Function.Injective p ∧ ∀ (i : Fin k), Nat.Prime (p i) ∧ p i ∣ n + ↑i + 1

There exists a constant c > 0 such that for all n, if k < c * (log n / (log (log n))) ^ 3 → (∀ i < k, ¬ (n + i + 1).Prime), then there are distinct primes p₁, ... pₖ such that pᵢ ∣ n + i for all 1 ≤ i ≤ k. This is proved in [RST75]. There is no need to only consider sufficiently large n because one can always take c small enough so that k < c * (log n / (log (log n))) ^ 3 implies that k = 0 until n is large.