Erdős problem 379

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.