Is it true for any `c < 1` and all `n` sufficiently large, for all `1 ≤ k < n`, `n.choose k`
has a divisor in `(cn, n]`? This is a variant of `erdos_387` and appears in [Gu04].
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
theorem erdos_387.variant : answer(sorry) ↔ ∀ c : ℝ, c < 1 → ∀ᶠ n : ℕ in atTop, ∀ k : ℕ, 1 ≤ k →
k < n → ∃ d : ℕ, (d : ℝ) ∈ Set.Ioc (c * n) n ∧ d ∣ n.choose k
