Erdős Problem 1095

References:

• erdosproblems.com/1095
• [EES74] Ecklund, Jr., E. F. and Erd\H{o}s, P. and Selfridge, J. L., A new function associated with the prime factors of {$(\sp{n}\sb{k})$}. Math. Comp. (1974), 647--649.
• [ELS93] Erdős, P. and Lacampagne, C. B. and Selfridge, J. L., Estimates of the least prime factor of a binomial coefficient. Math. Comp. (1993), 215--224.
• [GrRa96] Granville, Andrew and Ramaré, Olivier, Explicit bounds on exponential sums and the scarcity of squarefree binomial coefficients. Mathematika (1996), 73--107.
• [Ko99b] Konyagin, S. V., Estimates of the least prime factor of a binomial coefficient. Mathematika (1999), 41--55.
• [SSW20] Sorenson, Brianna and Sorenson, Jonathan and Webster, Jonathan, An algorithm and estimates for the {E}rdős-{S}elfridge function. (2020), 371--385.

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

Let $g(k)>k+1$ be the smallest $n$ such that all prime factors of $\binom{n}{k}$ are $>k$.

Equations

• Erdos1095.g k = sInf {m : ℕ | k + 1 < m ∧ k < (m.choose k).minFac}

theorem Erdos1095.erdos_1095.variants.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.variants.upper_conjecture : ∃ (f : ℕ → ℝ), Filter.Tendsto f Filter.atTop (nhds 0) ∧ ∀ᶠ (k : ℕ) in Filter.atTop, ↑(g k) ≤ Real.exp (↑k * (1 + f k))

Ecklund, Erdős, and Selfridge [EES74] conjectured $g(k)\leq \exp((1+o(1))k)$.

theorem Erdos1095.erdos_1095.variants.lower_conjecture : ∃ c > 0, ∀ᶠ (k : ℕ) in Filter.atTop, ↑(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.variants.log_equivalent : Asymptotics.IsEquivalent Filter.atTop (fun (k : ℕ) => Real.log ↑(g k)) fun (k : ℕ) => ↑k / Real.log ↑k

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