Erdős Problem 961

Reference: erdosproblems.com/961

noncomputable def Erdos961.Erdos961Prop (k n : ℕ) : Prop

Equations

• Erdos961.Erdos961Prop k n = ∀ m ≥ k + 1, ∃ i ∈ Set.Ico m (m + n), i ∉ (k + 1).smoothNumbers

theorem Erdos961.erdos_961.sylvester_schur (k : ℕ) : Erdos961Prop k k

Sylvester and Schur [Er34] proved that every set of $k$ consecutive integers greater than $k$ contains an integer divisible by a prime greater than $k$, i.e. not $(k+1)$-smooth.

theorem Erdos961.erdos_961.well_defined (k : ℕ) : ∃ (n : ℕ), Erdos961Prop k n

noncomputable def Erdos961.f (k : ℕ) : ℕ

For $k$, let $f(k)$ be the minimal $n$ such that every set of $n$ consecutive integers $>k$ contains an integer divisible by a prime $>k$, i.e. not $(k+1)$-smooth.

Equations

• Erdos961.f k = Nat.find ⋯

theorem Erdos961.erdos_961 : sorry ↔ ∃ C > 0, ∀ᶠ (k : ℕ) in Filter.atTop, ↑(f k) < Real.log ↑k ^ C

It is conjectured that $f(k) \ll (\log k)^O(1)$.

theorem Erdos961.erdos_961.erdos_upper_bound : ∀ᶠ (k : ℕ) in Filter.atTop, ↑(f k) < 3 * ↑k / Real.log ↑k

Erdos [Er55d] proved $f(k) < 3 \frac{k}{\log k}$ for sufficiently large $k$.

theorem Erdos961.erdos_961.jutila_ramachandra_shorey_upper_bound : (fun (k : ℕ) => ↑(f k)) =O[Filter.atTop] fun (k : ℕ) => Real.log (Real.log (Real.log ↑k)) / Real.log (Real.log ↑k) * (↑k / Real.log ↑k)

Jutila [Ju74], and Ramachandra--Shorey [RaSh73] proved a stronger upper bound $f(k) \ll \frac{\log \log \log k}{\log \log k} \frac{k}{\log k}$.