Erdős Problem 457

Reference: erdosproblems.com/457

theorem 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\leq (2 + \epsilon)\log n$ divide $$ \prod_{1\leq i\leq \log n} (n + i)? $$

@[reducible, inline]

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

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

Equations

• q n k = Nat.find ⋯

theorem 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\leq i\leq k}(n + i)$. This problem asks whether $q(n,\log n)\geq(2+\epsilon)\log n$ infinitely often.

theorem 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)\geq(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$?