/-
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 1063
References:
[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, Jean-Marie, Problems and Solutions: Solutions of Advanced Problems: 6447. Amer. Math. Monthly 92 (1985), 435-436.
open Filter Realopen scoped Nat Topologynamespace Erdos1063Let $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 than Cambie's $n_k \leq k \cdot \operatorname{lcm}(1, \dotsc, k-1)$.
The comparator takes its least common multiple in ℕ and casts the result. Writing the
ascription as ((… ).lcm (fun n : ℕ => n) : ℝ) instead puts it on the Finset.lcm
application, so the coercion lands on n and the lcm is taken in ℝ, where lcm of
non-zero elements is 1 and the whole comparator collapses to k.
@[category research open, AMS 11]
theorem 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 id : ℕ) : ℝ) := ⊢ 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 id)
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 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).
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⊢ 12 ≤ b
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 ≤ bh: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]), since $\binom{k!}{k}$ is divisible by $k! - i$ for $1 \le i < k$.
The hypothesis 3 ≤ k is necessary. At $k = 2$ the bound is false: $n_2 = 4$ and $2! = 2$.
@[category research solved, AMS 11]
theorem 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)$.
The hypothesis 3 ≤ k is necessary here too. At $k = 2$ the right hand side is
$2 \cdot \operatorname{lcm}(1) = 2$, while $n_2 = 4$.
The source writes the bound as $k[2, 3, \dotsc, k-1]$. That agrees with the range used here, because including $1$ does not change a least common multiple.
@[category research solved, AMS 11]
theorem 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 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