Skip to content

Erdős problem 387

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 statement3 of 4

Is it true for any c<1c < 1 and all nn sufficiently large, for all 1≤k<n1 \leq k < n, (nk)\binom{n}{k} has a divisor in (cn,n](cn, n]?

This variant appears in [Gu04]. Bui, Naprienko, Pratt, and Zaharescu [BNPZ26] answered it negatively.

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