Number theory

Erdős 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}?

References

erdosproblems.com/396

No one has attempted this yet.

Formal statement

Lean type

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

What you must prove

import FormalConjectures.ErdosProblems.«396»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos396.erdos_396" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/396.lean

Source type SHA-256: sha256:ca1aa2d9d9356095ec473de369398e4ea0eecba8e73b9d5dc1ff2d6964629b01
Task id: fc-379fc029-erdos396-erdos-396-c3a92ed41b-formalized-v1
Task commitment: sha256:cdc504584cdd8b47c1ba616d5293d6e7e2488766839be3c2f6c9af875e6254b2

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.