Erdős Problem 379

Reference: erdosproblems.com/379

theorem Erdos379.erdos_379 : Filter.limsup (fun (n : ℕ) => ↑(Erdos379.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$. See solution in the comments on erdosproblems.com, and https://github.com/teorth/analysis/blob/3522239c96742eaa0b3e8db9e7d41fe4c4907b37/analysis/Analysis/Misc/erdos_379.lean#L111