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$ .

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

379.lean

Retained formal statement1 of 1

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.

FormalConjectures/ErdosProblems/379.leanErdos379.erdos_3791 lineExact file

1Filter.limsup (fun n => ↑(Erdos379.S n)) Filter.atTop = ⊤

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.