Erdős Problem 683

References:

• erdosproblems.com/683
• [Er34] Erdős, Paul, A Theorem of Sylvester and Schur. J. London Math. Soc. (1934), 282--288.
• [Er55d] Erdős, P., On consecutive integers. Nieuw Arch. Wisk. (3) (1955), 124--128.
• [Er79d] Erdős, P., Some unconventional problems in number theory. Acta Math. Acad. Sci. Hungar. (1979), 71-80.

def Erdos683.P (n k : ℕ) : ℕ

Let $P(n, k)$ be the largest prime factor of $\binom{n}{k}$.

Equations

• Erdos683.P n k = (n.choose k).primeFactors.sup id

theorem Erdos683.erdos_683 : True ↔ ∃ c > 0, ∀ (n k : ℕ), 0 < k ∧ k < n → ↑(P n k) > min (↑n - ↑k + 1) (↑k ^ (1 + c))

There exists $c > 0$ such that $P(n, k) > \min\{n-k+1, k^{1 + c}\}$ for all $0 < k < n$.}

theorem Erdos683.erdos_683.variant.sylvester_schur (n k : ℕ) : 0 < k ∧ k ≤ n / 2 → P n k > k

Sylvester and Schur [Er34] proved that $P(n, k) > k$ for $k \le n/2$.

theorem Erdos683.erdos_683.variant.erdos_log : ∃ c > 0, ∀ (n k : ℕ), 0 < k ∧ k ≤ n / 2 → ↑(P n k) > c * ↑k * Real.log ↑k

Erdos [Er55d] improved this to $P(n, k) \gg k \log k $ for $k \le n/2$.

theorem Erdos683.erdos_683.variant.exp_sqrt : ∃ c > 0, ∀ (n k : ℕ), 0 < k ∧ k ≤ n / 2 → ↑(P n k) > Real.exp (c * √↑k)

Standard heuristics suggest that $P(n, k) > e^{c\sqrt{k}}$ for some constant $c > 0$.