/-
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 FormalConjecturesUtilErdős Problem 387
References:
[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 Filternamespace Erdos387Is 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 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 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].
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 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