1. FormalConjectures
  2. ErdosProblems
  3. «387»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 387

References:

    erdosproblems.com/387

    [ErGr76b] Erdős, P. and Graham, R. L., On the prime factors of ${n \choose k}$. Fibonacci Quart. (1976), 348-352.

    [Er78g] Erdős, Pál, On prime factors of binomial coefficients. II. Mat. Lapok (1978/82), 307-316.

    [ErGr80] Erdős, P. and Graham, R., Old and new problems and results in combinatorial number theory. Monographies de L'Enseignement Mathematique (1980).

    [Sc58] Schinzel, A., Sur un problème de P. Erdős. Colloq. Math. (1958), 198-204.

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

    [BNPZ26] Bui, H., Naprienko, S., Pratt, K., and Zaharescu, A. Binomial coefficients with divisors avoiding an interval. arXiv:2605.21221 (2026).

open Filter namespace Erdos387

Is there an absolute constant $c > 0$ such that, for all $1 \leq k < n$, the binomial coefficient $\binom{n}{k}$ has a divisor in $(cn, n]$?

Bui, Naprienko, Pratt, and Zaharescu [BNPZ26] answered this negatively.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_387 : answer(False) ↔ ∃ c : ℝ, 0 < c ∧ ∀ n k : ℕ, 1 ≤ k → k < n → ∃ d : ℕ, (d : ℝ) ∈ Set.Ioc (c * n) n ∧ d ∣ n.choose k := ⊢ False ↔ ∃ c, 0 < c ∧ ∀ (n k : ℕ), 1 ≤ k → k < n → ∃ d, ↑d ∈ Set.Ioc (c * ↑n) ↑n ∧ d ∣ n.choose k All goals completed! 🐙 @[category research solved, AMS 11] example : ∀ i < 15, ¬ 99215 - i ∣ Nat.choose 99215 15 := fun i hi => i:ℕhi:i < 15⊢ ¬99215 - i ∣ Nat.choose 99215 15 i:ℕhi:0 < 15⊢ ¬99215 - 0 ∣ Nat.choose 99215 15i:ℕhi:1 < 15⊢ ¬99215 - 1 ∣ Nat.choose 99215 15i:ℕhi:2 < 15⊢ ¬99215 - 2 ∣ Nat.choose 99215 15i:ℕhi:3 < 15⊢ ¬99215 - 3 ∣ Nat.choose 99215 15i:ℕhi:4 < 15⊢ ¬99215 - 4 ∣ Nat.choose 99215 15i:ℕhi:5 < 15⊢ ¬99215 - 5 ∣ Nat.choose 99215 15i:ℕhi:6 < 15⊢ ¬99215 - 6 ∣ Nat.choose 99215 15i:ℕhi:7 < 15⊢ ¬99215 - 7 ∣ Nat.choose 99215 15i:ℕhi:8 < 15⊢ ¬99215 - 8 ∣ Nat.choose 99215 15i:ℕhi:9 < 15⊢ ¬99215 - 9 ∣ Nat.choose 99215 15i:ℕhi:10 < 15⊢ ¬99215 - 10 ∣ Nat.choose 99215 15i:ℕhi:11 < 15⊢ ¬99215 - 11 ∣ Nat.choose 99215 15i:ℕhi:12 < 15⊢ ¬99215 - 12 ∣ Nat.choose 99215 15i:ℕhi:13 < 15⊢ ¬99215 - 13 ∣ Nat.choose 99215 15i:ℕhi:14 < 15⊢ ¬99215 - 14 ∣ Nat.choose 99215 15 i:ℕhi:0 < 15⊢ ¬99215 - 0 ∣ Nat.choose 99215 15i:ℕhi:1 < 15⊢ ¬99215 - 1 ∣ Nat.choose 99215 15i:ℕhi:2 < 15⊢ ¬99215 - 2 ∣ Nat.choose 99215 15i:ℕhi:3 < 15⊢ ¬99215 - 3 ∣ Nat.choose 99215 15i:ℕhi:4 < 15⊢ ¬99215 - 4 ∣ Nat.choose 99215 15i:ℕhi:5 < 15⊢ ¬99215 - 5 ∣ Nat.choose 99215 15i:ℕhi:6 < 15⊢ ¬99215 - 6 ∣ Nat.choose 99215 15i:ℕhi:7 < 15⊢ ¬99215 - 7 ∣ Nat.choose 99215 15i:ℕhi:8 < 15⊢ ¬99215 - 8 ∣ Nat.choose 99215 15i:ℕhi:9 < 15⊢ ¬99215 - 9 ∣ Nat.choose 99215 15i:ℕhi:10 < 15⊢ ¬99215 - 10 ∣ Nat.choose 99215 15i:ℕhi:11 < 15⊢ ¬99215 - 11 ∣ Nat.choose 99215 15i:ℕhi:12 < 15⊢ ¬99215 - 12 ∣ Nat.choose 99215 15i:ℕhi:13 < 15⊢ ¬99215 - 13 ∣ Nat.choose 99215 15i:ℕhi:14 < 15⊢ ¬99215 - 14 ∣ Nat.choose 99215 15 All goals completed! 🐙

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

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_387.variants.schinzel : answer(sorry) ↔ ∀ᶠ k in atTop, ¬ IsPrimePow k → ∃ n : ℕ, ∀ i < k, ¬ n - i ∣ n.choose k := ⊢ True ↔ ∀ᶠ (k : ℕ) in atTop, ¬IsPrimePow k → ∃ n, ∀ i < k, ¬n - i ∣ n.choose k All goals completed! 🐙

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

@[category research solved, AMS 11] theorem erdos_387.variants.easy {n : ℕ} {k : ℕ} (hn : 1 ≤ n) (hk : k ≤ n) : ∃ d : ℕ, (d : ℝ) ∈ Set.Icc (n / k : ℝ) n ∧ d ∣ n.choose k := n:ℕk:ℕhn:1 ≤ nhk:k ≤ n⊢ ∃ d, ↑d ∈ Set.Icc (↑n / ↑k) ↑n ∧ d ∣ n.choose k n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:k = 0⊢ ∃ d, ↑d ∈ Set.Icc (↑n / ↑k) ↑n ∧ d ∣ n.choose kn:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ ∃ d, ↑d ∈ Set.Icc (↑n / ↑k) ↑n ∧ d ∣ n.choose k n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:k = 0⊢ ∃ d, ↑d ∈ Set.Icc (↑n / ↑k) ↑n ∧ d ∣ n.choose kn:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ ∃ d, ↑d ∈ Set.Icc (↑n / ↑k) ↑n ∧ d ∣ n.choose k n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ ∃ d, (↑n / ↑k ≤ ↑d ∧ d ≤ n) ∧ d ∣ n.choose k n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ ↑n / ↑k ≤ ↑((n.choose k).gcd n)n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ (n.choose k).gcd n ≤ n n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ ↑n / ↑k ≤ ↑((n.choose k).gcd n) n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ ↑n ≤ ↑((n.choose k).gcd n) * ↑k n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ n ≤ (n.choose k).gcd n * k n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ n ≤ (n.choose k * k).gcd (n * k) n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ 0 < (n.choose k * k).gcd (n * k)n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ n.choose k * k = n * (n - 1).choose (k - 1) n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ 0 < (n.choose k * k).gcd (n * k) exact Nat.gcd_pos_of_pos_right _ (n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ 0 < n * k All goals completed! 🐙) n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ n.choose k * k = n * (n - 1).choose (k - 1) k:ℕh✝:¬k = 0hn:1 ≤ 0hk:k ≤ 0⊢ Nat.choose 0 k * k = 0 * (0 - 1).choose (k - 1)k:ℕh✝:¬k = 0n✝:ℕhn:1 ≤ n✝ + 1hk:k ≤ n✝ + 1⊢ (n✝ + 1).choose k * k = (n✝ + 1) * (n✝ + 1 - 1).choose (k - 1) k:ℕh✝:¬k = 0hn:1 ≤ 0hk:k ≤ 0⊢ Nat.choose 0 k * k = 0 * (0 - 1).choose (k - 1)k:ℕh✝:¬k = 0n✝:ℕhn:1 ≤ n✝ + 1hk:k ≤ n✝ + 1⊢ (n✝ + 1).choose k * k = (n✝ + 1) * (n✝ + 1 - 1).choose (k - 1) n✝:ℕhn:1 ≤ n✝ + 1h✝:¬0 = 0hk:0 ≤ n✝ + 1⊢ (n✝ + 1).choose 0 * 0 = (n✝ + 1) * (n✝ + 1 - 1).choose (0 - 1)n✝¹:ℕhn:1 ≤ n✝ + 1n✝:ℕh✝:¬n✝ + 1 = 0hk:n✝ + 1 ≤ n✝¹ + 1⊢ (n✝¹ + 1).choose (n✝ + 1) * (n✝ + 1) = (n✝¹ + 1) * (n✝¹ + 1 - 1).choose (n✝ + 1 - 1) hn:1 ≤ 0h✝:¬0 = 0hk:0 ≤ 0⊢ Nat.choose 0 0 * 0 = 0 * (0 - 1).choose (0 - 1)hn:1 ≤ 0n✝:ℕh✝:¬n✝ + 1 = 0hk:n✝ + 1 ≤ 0⊢ Nat.choose 0 (n✝ + 1) * (n✝ + 1) = 0 * (0 - 1).choose (n✝ + 1 - 1)n✝:ℕhn:1 ≤ n✝ + 1h✝:¬0 = 0hk:0 ≤ n✝ + 1⊢ (n✝ + 1).choose 0 * 0 = (n✝ + 1) * (n✝ + 1 - 1).choose (0 - 1)n✝¹:ℕhn:1 ≤ n✝ + 1n✝:ℕh✝:¬n✝ + 1 = 0hk:n✝ + 1 ≤ n✝¹ + 1⊢ (n✝¹ + 1).choose (n✝ + 1) * (n✝ + 1) = (n✝¹ + 1) * (n✝¹ + 1 - 1).choose (n✝ + 1 - 1) All goals completed! 🐙 n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ (n.choose k).gcd n ≤ n exact Nat.le_of_dvd (n:ℕk:ℕhn:1 ≤ nhk:k ≤ nh✝:¬k = 0⊢ 0 < n All goals completed! 🐙) (gcd_dvd_right _ _)

Is it true for any $c < 1$ and all $n$ sufficiently large, for all $1 \leq k < n$, $\binom{n}{k}$ has a divisor in $(cn, n]$?

This variant appears in [Gu04]. Bui, Naprienko, Pratt, and Zaharescu [BNPZ26] answered it negatively.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_387.variants.guy : answer(False) ↔ ∀ c : ℝ, c < 1 → ∀ᶠ n : ℕ in atTop, ∀ k : ℕ, 1 ≤ k → k < n → ∃ d : ℕ, (d : ℝ) ∈ Set.Ioc (c * n) n ∧ d ∣ n.choose k := ⊢ False ↔ ∀ c < 1, ∀ᶠ (n : ℕ) in atTop, ∀ (k : ℕ), 1 ≤ k → k < n → ∃ d, ↑d ∈ Set.Ioc (c * ↑n) ↑n ∧ d ∣ n.choose k All goals completed! 🐙 end Erdos387