Erdős problem 379 · problems.science

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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/379.lean

Formal Conjectures

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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:379
PLBY Lean proofsErdosProblems.Erdos379

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

AI building on literature
Erdős AI contributions wiki · 21 Dec, 2025
Machine
Seed Prover 1.5
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science