Erdős problem 396

Is it true that for every $k$ there exists $n$ such that $\prod_{0\leq i\leq k}(n-i) \mid \binom{2n}{n}?$

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

396.lean

Retained formal statement1 of 1

Is it true that for every $k$ there exists $n$ such that $\prod_{0\leq i\leq k}(n-i) \mid \binom{2n}{n}?$

FormalConjectures/ErdosProblems/396.leanErdos396.erdos_3961 lineExact file

1True ↔ ∀ (k : ℕ), ∃ n, n.descFactorial (k + 1) ∣ n.centralBinom

OpenStatement only, no proof