Skip to content

Erdős problem 387

Start work

Is there an absolute constant c>0c > 0 such that, for all 1≤k<n1 \leq k < n, the binomial coefficient (nk)\binom{n}{k} has a divisor in (cn,n](cn, n]?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

387.lean

Retained formal statement1 of 4

Is there an absolute constant c>0c > 0 such that, for all 1≤k<n1 \leq k < n, the binomial coefficient (nk)\binom{n}{k} has a divisor in (cn,n](cn, n]?

Bui, Naprienko, Pratt, and Zaharescu [BNPZ26] answered this negatively.

FormalConjectures/ErdosProblems/387.leanErdos387.erdos_3871 lineExact file
False ↔ ∃ c, 0 < c ∧ ∀ (n k : ℕ), 1 ≤ k → k < n → ∃ d, ↑d ∈ Set.Ioc (c * ↑n) ↑n ∧ d ∣ n.choose k
SolvedStatement only, no proof