Erdős Problem 962

References:

• erdosproblems.com/962
• [Er65] Erdős, P., Extremal problems in number theory. Proc. Sympos. Pure Math., Vol. VIII (1965), 181-189.
• [Er76e] Erdős, P., Problems and results on consecutive integers. Publ. Math. Debrecen (1976), 271-282.
• Tang
• Tao

def Erdos962.Erdos962Prop (n k : ℕ) : Prop

Erdos962Prop n k : there exists $m \le n$ such that each of $m+1, \ldots, m+k$ has a prime divisor strictly larger than $k$.

Equations

• Erdos962.Erdos962Prop n k = ∃ m ≤ n, ∀ i ∈ Set.Icc 1 k, ∃ (p : ℕ), Nat.Prime p ∧ k < p ∧ p ∣ m + i

noncomputable def Erdos962.k (n : ℕ) : ℕ

Let $k(n)$ be the maximal $k$ such that there exists $m \le n$ with $m+1, \ldots, m+k$ each divisible by a prime $> k$.

Equations

• Erdos962.k n = Nat.findGreatest (fun (k : ℕ) => Erdos962.Erdos962Prop n k) n

theorem Erdos962.erdos_962 : True ↔ ∃ (ε : ℕ → ℝ), (∀ δ > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |ε n| < δ) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, Real.log ↑(k n) ≤ (Real.log ↑n).rpow (1 / 2 + ε n)

Main conjecture:

$\log k(n) \le (\log n)^{(1/2 + o(1))}$

theorem Erdos962.erdos_962.variants.tang_lower_bound : ∃ (ε : ℕ → ℝ), (∀ δ > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |ε n| < δ) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, (1 / √2 - ε n) * √(Real.log ↑n * Real.log (Real.log ↑n)) ≤ Real.log ↑(k n)

Tang's lower bound [Tang]:

$\log k(n) \ge (1/\sqrt{2} - o(1)) * \sqrt{\log n * \log \log n}$

theorem Erdos962.erdos_962.variants.tao_upper_bound : ∃ (ε : ℕ → ℝ), (∀ δ > 0, ∀ᶠ (n : ℕ) in Filter.atTop, |ε n| < δ) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(k n) ≤ (1 + ε n) * √↑n

Tao's upper bound [Tao]:

$k(n) \le (1 + o(1)) * n^{1/2}$