Erdős Problem 379

Reference: erdosproblems.com/379

noncomputable def Erdos379.S (n : ℕ) : ℕ

Equations

• Erdos379.S n = sSup {s : ℕ | ∀ k ∈ Finset.Ico 1 n, ∃ (p : ℕ), Nat.Prime p ∧ p ^ s ∣ n.choose k}

theorem Erdos379.erdos_379 : Filter.limsup (fun (n : ℕ) => ↑(S n)) Filter.atTop = ⊤

Let $S(n)$ denote the largest integer such that, for all $1 ≤ k < n$, the binomial coefficient $\binom{n}{k}$ is divisible by $p^S(n)$ for some prime $p$ (depending on $k$).Then $\limsup S(n) = \infty$.

This was formalized in Lean by Tao.