Erdős Problem 1095

Reference: erdosproblems.com/1095

noncomputable def Erdos1095.g (k : ℕ) : ℕ

Let $g(k)>k+1$ be maximal such that if $n\leq g(k)$ then $\binom{n}{k}$ is divisible by a prime $\leq k$. Estimate $g(k)$.

Equations

• Erdos1095.g k = sSup {m : ℕ | ∀ n ∈ Set.Ioc k m, ∃ p ≤ k, Nat.Prime p ∧ p ∣ n.choose k}

theorem Erdos1095.erdos_1095_lower_solved : ∃ c > 0, (fun (k : ℕ) => Real.exp (c * Real.log ↑k ^ 2)) =O[Filter.atTop] fun (k : ℕ) => ↑(g k)

The current record is[g(k) \gg \exp(c(\log k)^2)]for some $c>0$, due to Konyagin Ko99b.

theorem Erdos1095.erdos_1095_upper_conjecture : ∃ (f : ℕ → ℝ), Filter.Tendsto f Filter.atTop (nhds 0) ∧ ∀ (k : ℕ), ↑(g k) ≤ Real.exp (↑k ^ (1 + f k))

Ecklund, Erdős, and Selfridge conjectured $g(k)\leq \exp(k^{1+o(1)})$ EES74

theorem Erdos1095.erdos_1095_lower_conjecture : ∃ c > 0, ∀ (k : ℕ), ↑(g k) ≥ Real.exp (c * ↑k / Real.log ↑k)

Erdős, Lacampagne, and Selfridge ELS93 write 'it is clear to every right-thinking person' that $g(k)\geq\exp(c\frac{k}{\log k})$ for some constant $c>0$.

theorem Erdos1095.erdos_1095_log_equivalent : Asymptotics.IsEquivalent Filter.atTop (fun (k : ℕ) => Real.log ↑(g k)) fun (k : ℕ) => ↑k / Real.log ↑k

Sorenson, Sorenson, and Webster give heuristic evidence that [\log g(k) \asymp \frac{k}{\log k}.]