Erdős Problem 387

References:

• erdosproblems.com/387
• [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), xviii+437.
• [Fa66] Faulkner, M. "On a theorem of Sylvester and Schur." Journal of the London Mathematical Society 1.1 (1966): 107-110.

theorem Erdos387.erdos_387 : sorry ↔ ∃ (c : ℝ), 0 < c ∧ ∀ (n k : ℕ), 1 ≤ k → k < n → ∃ (d : ℕ), ↑d ∈ Set.Ioc (c * ↑n) ↑n ∧ d ∣ n.choose k

Is there an absolute constant c > 0 such that, for all 1 ≤ k < n, the binomial coefficient n.choose k has a divisor in (cn, n]?

theorem Erdos387.erdos_387.schinzel : sorry ↔ ∀ᶠ (k : ℕ) in Filter.atTop, ¬IsPrimePow k → ∃ (n : ℕ), ∀ i < k, ¬n - i ∣ n.choose k

The following is Schinzel's conjecture, which appears in [Gu04].

theorem Erdos387.erdos_387.easy {n k : ℕ} (hn : 1 ≤ n) (hk : k ≤ n) : ∃ (d : ℕ), ↑d ∈ Set.Icc (↑n / ↑k) ↑n ∧ d ∣ n.choose k

It is easy to see that n.choose k has a divisor in [n / k, n].

theorem Erdos387.erdos_387.variant : sorry ↔ ∀ c < 1, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (k : ℕ), 1 ≤ k → k < n → ∃ (d : ℕ), ↑d ∈ Set.Ioc (c * ↑n) ↑n ∧ d ∣ n.choose k

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].