Erdős Problem 457

Reference: erdosproblems.com/457

theorem Erdos457.erdos_457 : (∃ ε > 0, {n : ℕ | ∀ (p : ℕ), ↑p ≤ (2 + ε) * Real.log ↑n → Nat.Prime p → p ∣ ∏ i ∈ Finset.Icc 1 ⌊Real.log ↑n⌋₊, (n + i)}.Infinite) ↔ sorry

Is there some $\epsilon > 0$ such that there are infinitely many $n$ where all primes $p \le (2 + \epsilon) \log n$ divide $$ \prod_{1 \le i \le \log n} (n + i)? $$

@[reducible, inline]

noncomputable abbrev Erdos457.q (n : ℕ) (k : ℝ) : ℕ

Let $q(n, k)$ denote the least prime which does not divide $\prod_{1 \le i \le k}(n + i)$.

Equations

• Erdos457.q n k = Nat.find ⋯

theorem Erdos457.erdos_457.variants.qnk : (∃ ε > 0, {n : ℕ | (2 + ε) * Real.log ↑n ≤ ↑(q n (Real.log ↑n))}.Infinite) ↔ sorry

More generally, let $q(n, k)$ denote the least prime which does not divide $\prod_{1 \le i \le k}(n + i)$. This problem asks whether $q(n, \log n) \ge (2 + \epsilon) \log n$ infinitely often.

theorem Erdos457.erdos_457.variants.one_sub : (∃ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(q n (Real.log ↑n)) < (1 - ε) * Real.log ↑n ^ 2) ↔ sorry

Taking $n$ to be the product of primes between $\log n$ and $(2 + o(1)) \log n$ gives an example where $$ q(n, \log n) \ge (2 + o(1)) \log n. $$ Can one prove that $q(n, \log n) < (1 - \epsilon) (\log n)^2$ for all large $n$ and some $\epsilon > 0$?