1. FormalConjectures
  2. ErdosProblems
  3. «1063»
/- 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 1063

References:

    erdosproblems.com/1063

    [ErSe83] Erdos, P. and Selfridge, J. L., Problem 6447. Amer. Math. Monthly (1983), 710.

    [Gu04] Guy, Richard K., Unsolved problems in number theory. (2004), Problem B31.

    [Mo85] Monier (1985). No reference found.

open Filter Realopen scoped Nat Topology namespace Erdos1063

Let $n_k$ be the least $n \ge 2k$ such that all but one of the integers $n - i$ with $0 \le i < k$ divide $\binom{n}{k}$.

noncomputable def n (k : ℕ) : ℕ := sInf {m | 2 * k ≤ m ∧ ∃ i0 < k, ¬ (m - i0) ∣ m.choose k ∧ ∀ i < k, i ≠ i0 → (m - i) ∣ m.choose k}

Estimate $n_k$ by finding a better upper bound.

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_1063.better_upper : let upper_bound : ℕ → ℝ := answer(sorry) (fun k => (n k : ℝ)) =O[atTop] upper_bound ∧ upper_bound =o[atTop] fun k => (k : ℝ) * ((Finset.Icc 1 (k - 1)).lcm (fun n : ℕ => n) : ℝ) := ⊢ let upper_bound := sorry; (fun k => ↑(n k)) =O[atTop] upper_bound ∧ upper_bound =o[atTop] fun k => ↑k * (Finset.Icc 1 (k - 1)).lcm fun n => ↑n All goals completed! 🐙

Erdős and Selfridge noted that, for $n \ge 2k$ with $k \ge 2$, at least one of the numbers $n - i$ for $0 \le i < k$ fails to divide $\binom{n}{k}$ ([ErSe83]).

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_1063.variants.exists_exception {n k : ℕ} (hk : 2 ≤ k) (h : 2 * k ≤ n) : ∃ i < k, ¬ (n - i) ∣ n.choose k := n:ℕk:ℕhk:2 ≤ kh:2 * k ≤ n⊢ ∃ i < k, ¬n - i ∣ n.choose k All goals completed! 🐙

The initial values satisfy $n_2 = 4$, $n_3 = 6$, $n_4 = 9$, and $n_5 = 12$ ([Gu04], Problem B31).

@[category research solved, AMS 11] theorem erdos_1063.variants.small_values : n 2 = 4 ∧ n 3 = 6 ∧ n 4 = 9 ∧ n 5 = 12 := ⊢ n 2 = 4 ∧ n 3 = 6 ∧ n 4 = 9 ∧ n 5 = 12 ⊢ n 2 = 4⊢ n 3 = 6⊢ n 4 = 9⊢ n 5 = 12 ⊢ n 2 = 4 -- n 2 = 4 : every element of the set is ≥ 2 * 2 = 4, and 4 itself lies in the set ⊢ n 2 ≤ 4⊢ 4 ≤ n 2 ⊢ n 2 ≤ 4 exact Nat.sInf_le (⊢ 4 ∈ {m | 2 * 2 ≤ m ∧ ∃ i0 < 2, ¬m - i0 ∣ m.choose 2 ∧ ∀ i < 2, i ≠ i0 → m - i ∣ m.choose 2} All goals completed! 🐙) ⊢ 4 ≤ n 2 apply le_csInf ⟨4, ⊢ 4 ∈ {m | 2 * 2 ≤ m ∧ ∃ i0 < 2, ¬m - i0 ∣ m.choose 2 ∧ ∀ i < 2, i ≠ i0 → m - i ∣ m.choose 2} All goals completed! 🐙⟩ b:ℕhb:b ∈ {m | 2 * 2 ≤ m ∧ ∃ i0 < 2, ¬m - i0 ∣ m.choose 2 ∧ ∀ i < 2, i ≠ i0 → m - i ∣ m.choose 2}⊢ 4 ≤ b b:ℕhb:b ∈ {m | 2 * 2 ≤ m ∧ ∃ i0 < 2, ¬m - i0 ∣ m.choose 2 ∧ ∀ i < 2, i ≠ i0 → m - i ∣ m.choose 2}this:2 * 2 ≤ b := hb.left⊢ 4 ≤ b All goals completed! 🐙 ⊢ n 3 = 6 -- n 3 = 6 ⊢ n 3 ≤ 6⊢ 6 ≤ n 3 ⊢ n 3 ≤ 6 exact Nat.sInf_le (⊢ 6 ∈ {m | 2 * 3 ≤ m ∧ ∃ i0 < 3, ¬m - i0 ∣ m.choose 3 ∧ ∀ i < 3, i ≠ i0 → m - i ∣ m.choose 3} All goals completed! 🐙) ⊢ 6 ≤ n 3 apply le_csInf ⟨6, ⊢ 6 ∈ {m | 2 * 3 ≤ m ∧ ∃ i0 < 3, ¬m - i0 ∣ m.choose 3 ∧ ∀ i < 3, i ≠ i0 → m - i ∣ m.choose 3} All goals completed! 🐙⟩ b:ℕhb:b ∈ {m | 2 * 3 ≤ m ∧ ∃ i0 < 3, ¬m - i0 ∣ m.choose 3 ∧ ∀ i < 3, i ≠ i0 → m - i ∣ m.choose 3}⊢ 6 ≤ b b:ℕhb:b ∈ {m | 2 * 3 ≤ m ∧ ∃ i0 < 3, ¬m - i0 ∣ m.choose 3 ∧ ∀ i < 3, i ≠ i0 → m - i ∣ m.choose 3}this:2 * 3 ≤ b := hb.left⊢ 6 ≤ b All goals completed! 🐙 ⊢ n 4 = 9 -- n 4 = 9 : the only candidate below 9 is m = 8, where both 8 and 6 fail to divide C(8,4) = 70 ⊢ n 4 ≤ 9⊢ 9 ≤ n 4 ⊢ n 4 ≤ 9 exact Nat.sInf_le (⊢ 9 ∈ {m | 2 * 4 ≤ m ∧ ∃ i0 < 4, ¬m - i0 ∣ m.choose 4 ∧ ∀ i < 4, i ≠ i0 → m - i ∣ m.choose 4} All goals completed! 🐙) ⊢ 9 ≤ n 4 apply le_csInf ⟨9, ⊢ 9 ∈ {m | 2 * 4 ≤ m ∧ ∃ i0 < 4, ¬m - i0 ∣ m.choose 4 ∧ ∀ i < 4, i ≠ i0 → m - i ∣ m.choose 4} All goals completed! 🐙⟩ b:ℕhb:b ∈ {m | 2 * 4 ≤ m ∧ ∃ i0 < 4, ¬m - i0 ∣ m.choose 4 ∧ ∀ i < 4, i ≠ i0 → m - i ∣ m.choose 4}⊢ 9 ≤ b have hb8 : 8 ≤ b := ⊢ n 2 = 4 ∧ n 3 = 6 ∧ n 4 = 9 ∧ n 5 = 12 b:ℕhb:b ∈ {m | 2 * 4 ≤ m ∧ ∃ i0 < 4, ¬m - i0 ∣ m.choose 4 ∧ ∀ i < 4, i ≠ i0 → m - i ∣ m.choose 4}this:2 * 4 ≤ b := hb.left⊢ 8 ≤ b; All goals completed! 🐙 b:ℕhb:b ∈ {m | 2 * 4 ≤ m ∧ ∃ i0 < 4, ¬m - i0 ∣ m.choose 4 ∧ ∀ i < 4, i ≠ i0 → m - i ∣ m.choose 4}hb8:8 ≤ b := have this := hb.left; thish:¬9 ≤ b⊢ False b:ℕhb:b ∈ {m | 2 * 4 ≤ m ∧ ∃ i0 < 4, ¬m - i0 ∣ m.choose 4 ∧ ∀ i < 4, i ≠ i0 → m - i ∣ m.choose 4}hb8:8 ≤ b := have this := hb.left; thish:b < 9⊢ False b:ℕhb:8 ∈ {m | 2 * 4 ≤ m ∧ ∃ i0 < 4, ¬m - i0 ∣ m.choose 4 ∧ ∀ i < 4, i ≠ i0 → m - i ∣ m.choose 4}hb8:8 ≤ 8h:8 < 9⊢ False b:ℕhb:8 ∈ {m | 2 * 4 ≤ m ∧ ∃ i0 < 4, ¬m - i0 ∣ m.choose 4 ∧ ∀ i < 4, i ≠ i0 → m - i ∣ m.choose 4}hb8:8 ≤ 8h:8 < 9⊢ False exact absurd hb (b:ℕhb:8 ∈ {m | 2 * 4 ≤ m ∧ ∃ i0 < 4, ¬m - i0 ∣ m.choose 4 ∧ ∀ i < 4, i ≠ i0 → m - i ∣ m.choose 4}hb8:8 ≤ 8h:8 < 9⊢ 8 ∉ {m | 2 * 4 ≤ m ∧ ∃ i0 < 4, ¬m - i0 ∣ m.choose 4 ∧ ∀ i < 4, i ≠ i0 → m - i ∣ m.choose 4} All goals completed! 🐙) ⊢ n 5 = 12 -- n 5 = 12 : the candidates below 12 are m = 10, 11, both of which fail ⊢ n 5 ≤ 12⊢ 12 ≤ n 5 ⊢ n 5 ≤ 12 exact Nat.sInf_le (⊢ 12 ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5} All goals completed! 🐙) ⊢ 12 ≤ n 5 apply le_csInf ⟨12, ⊢ 12 ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5} All goals completed! 🐙⟩ b:ℕhb:b ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5}⊢ 12 ≤ b have hb10 : 10 ≤ b := ⊢ n 2 = 4 ∧ n 3 = 6 ∧ n 4 = 9 ∧ n 5 = 12 b:ℕhb:b ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5}this:2 * 5 ≤ b := hb.left⊢ 10 ≤ b; All goals completed! 🐙 b:ℕhb:b ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5}hb10:10 ≤ b := have this := hb.left; thish:¬12 ≤ b⊢ False b:ℕhb:b ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5}hb10:10 ≤ b := have this := hb.left; thish:b < 12⊢ False b:ℕhb:10 ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5}hb10:10 ≤ 10h:10 < 12⊢ Falseb:ℕhb:11 ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5}hb10:10 ≤ 11h:11 < 12⊢ False b:ℕhb:10 ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5}hb10:10 ≤ 10h:10 < 12⊢ False exact absurd hb (b:ℕhb:10 ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5}hb10:10 ≤ 10h:10 < 12⊢ 10 ∉ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5} All goals completed! 🐙) b:ℕhb:11 ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5}hb10:10 ≤ 11h:11 < 12⊢ False exact absurd hb (b:ℕhb:11 ∈ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5}hb10:10 ≤ 11h:11 < 12⊢ 11 ∉ {m | 2 * 5 ≤ m ∧ ∃ i0 < 5, ¬m - i0 ∣ m.choose 5 ∧ ∀ i < 5, i ≠ i0 → m - i ∣ m.choose 5} All goals completed! 🐙)

Monier observed that $n_k \le k!$ for $k \ge 3$ ([Mo85]). TODO: Find reference

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_1063.variants.monier_upper_bound {k : ℕ} (hk : 3 ≤ k) : n k ≤ k ! := k:ℕhk:3 ≤ k⊢ n k ≤ k ! All goals completed! 🐙

Cambie observed the improved bound $n_k \le k \cdot \operatorname{lcm}(1, \dotsc, k - 1)$.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_1063.variants.cambie_upper_bound {k : ℕ} (hk : 3 ≤ k) : n k ≤ k * (Finset.Icc 1 (k - 1)).lcm id := k:ℕhk:3 ≤ k⊢ n k ≤ k * (Finset.Icc 1 (k - 1)).lcm id All goals completed! 🐙

The least common multiple bound implies $n_k \le \exp((1 + o(1))k)$.

@[category research solved, AMS 11] theorem declaration uses 'sorry'erdos_1063.variants.exp_upper_bound : ∃ f : ℕ → ℝ, Tendsto f atTop (𝓝 0) ∧ ∀ k, (n k : ℝ) ≤ exp ((1 + f k) * k) := ⊢ ∃ f, Tendsto f atTop (𝓝 0) ∧ ∀ (k : ℕ), ↑(n k) ≤ rexp ((1 + f k) * ↑k) All goals completed! 🐙 end Erdos1063