Erdős problem 387
Is there an absolute constant such that, for all , the binomial coefficient has a divisor in ?
Sources
FormalConjectures/ErdosProblems/
387.lean
Retained formal statement
Is there an absolute constant such that, for all , the binomial coefficient has a divisor in ?
Bui, Naprienko, Pratt, and Zaharescu [BNPZ26] answered this negatively.
False ↔ ∃ c, 0 < c ∧ ∀ (n k : ℕ), 1 ≤ k → k < n → ∃ d, ↑d ∈ Set.Ioc (c * ↑n) ↑n ∧ d ∣ n.choose kSolvedStatement only, no proof