/-
Copyright 2025 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
open Finset SimpleGraphopen scoped Natnamespace Erdos835
variable {n k : ℕ}
The property that for a given $k$, the $k$-subsets of a $2k$-set can be colored with $k+1$ colors such that any $(k+1)$-subset contains all colors.
def Property (k : ℕ) : Prop :=
let K := {s : Finset (Fin (2 * k)) // s.card = k}
∃ c : K → Fin (k + 1),
∀ A : Finset (Fin (2 * k)), A.card = k + 1 →
(image c {s : K | s.val ⊂ A}) = (univ : Finset (Fin (k+1)))
Does there exist a $k>2$ such that the $k$-sized subsets of {1,...,2k} can be coloured with $k+1$ colours such that for every $A\subset {1,\ldots,2k}$ with $\lvert A\rvert=k+1$ all $k+1$ colours appear among the $k$-sized subsets of $A$?
@[category research open, AMS 5]
theorem erdos_835 : (∃ k > 2, Property k) ↔ answer(sorry) := ⊢ (∃ k > 2, Property k) ↔ True
All goals completed! 🐙
@[category test, AMS 5]
theorem property_iff_chromaticNumber (k : ℕ) (hk : 0 < k) :
(J(2 * k, k).chromaticNumber = k + 1) ↔
Property k := k:ℕhk:0 < k⊢ χ(J(2 * k, k)) = ↑k + 1 ↔ Property k
All goals completed! 🐙
Alternative statement of Erdős Problem 835 using the chromatic number of the Johnson graph. This is equivalent to asking whether there exists $k > 2$ such that the chromatic number of the Johnson graph $J(2k, k)$ is $k+1$.
@[category research open, AMS 5]
theorem erdos_835.variants.johnson : (∃ l,
-- making sure k > 2
letI k := l + 3
J(2 * k, k).chromaticNumber = k + 1) ↔ answer(sorry) := ⊢ (∃ l, χ(J(2 * (l + 3), l + 3)) = ↑(l + 3) + 1) ↔ True
All goals completed! 🐙
It is known that for $3 \leq k \leq 8$, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.
@[category research solved, AMS 5]
theorem johnsonGraph_2k_k_chromaticNumber_known_cases (k : ℕ) (hk : 3 ≤ k) (hk' : k ≤ 8) :
J(2 * k, k).chromaticNumber > k + 1 := k:ℕhk:3 ≤ khk':k ≤ 8⊢ χ(J(2 * k, k)) > ↑k + 1
All goals completed! 🐙
The smallest case not on this page is $k=9$: But that one can be solved as well: The chromatic number of $J(18, 9)$ is at least $11$.
@[category research solved, AMS 5]
theorem johnsonGraph_18_9_chromaticNumber : J(18, 9).chromaticNumber > 9 + 1 := ⊢ χ(J(18, 9)) > 9 + 1
All goals completed! 🐙
Johnson's upper bound on the maximum size A(n, d, w) of a n-dimensional binary code of
distance d and weight w is as follows:
If d > 2 * w, then A(n, d, w) = 1.
If d ≤ 2 * w, then A(n, d, w) ≤ ⌊n / w * A(n - 1, d, w - 1)⌋.
def johnsonBound : ℕ → ℕ → ℕ → ℕ
| 0, _d, _w => 1
| _n, _d, 0 => 1
| n + 1, d, w + 1 => if 2 * (w + 1) < d then 1 else (n + 1) * johnsonBound n d w / (w + 1)Johnson's bound for the independence number of the Johnson graph.
@[category research solved, AMS 5]
lemma indepNum_johnson_le_johnsonBound : α(J(n, k)) ≤ johnsonBound n 4 k := sorryJohnson's bound for the chromatic number of the Johnson graph.
@[category research solved, AMS 5]
lemma div_johnsonBound_le_chromaticNum_johnson :
⌈(n.choose k / johnsonBound n 4 k : ℚ≥0)⌉₊ ≤ χ(J(n, k)) := n:ℕk:ℕ⊢ ↑⌈↑(n.choose k) / ↑(johnsonBound n 4 k)⌉₊ ≤ χ(J(n, k))
n:ℕk:ℕhnk:n < k⊢ ↑⌈↑(n.choose k) / ↑(johnsonBound n 4 k)⌉₊ ≤ χ(J(n, k))n:ℕk:ℕhkn:k ≤ n⊢ ↑⌈↑(n.choose k) / ↑(johnsonBound n 4 k)⌉₊ ≤ χ(J(n, k))
n:ℕk:ℕhnk:n < k⊢ ↑⌈↑(n.choose k) / ↑(johnsonBound n 4 k)⌉₊ ≤ χ(J(n, k)) All goals completed! 🐙
have : Nonempty {s : Finset (Fin n) // #s = k} := n:ℕk:ℕ⊢ ↑⌈↑(n.choose k) / ↑(johnsonBound n 4 k)⌉₊ ≤ χ(J(n, k))
simpa [Finset.Nonempty] using Finset.powersetCard_nonempty (s := .univ).2 <| n:ℕk:ℕhkn:k ≤ n⊢ k ≤ #univ All goals completed! 🐙
grw [← card_div_indepNum_le_chromaticNumber, indepNum_johnson_le_johnsonBoundn:ℕk:ℕhkn:k ≤ nthis:Nonempty { s // #s = k } :=
Eq.mpr (id nonempty_subtype._simp_1)
(Eq.mp
(congrArg Exists
(funext fun x =>
Eq.trans mem_powersetCard._simp_1
(Eq.trans (congrArg (fun x_1 => x_1 ∧ #x = k) (subset_univ._simp_1 x)) (true_and (#x = k)))))
(powersetCard_nonempty.mpr (Eq.mpr (id (congrArg (LE.le k) (Fintype.card_fin n))) hkn)))⊢ ↑⌈↑(n.choose k) / ↑(johnsonBound n 4 k)⌉₊ ≤ ↑⌈↑(Nat.card { s // #s = k }) / ↑(johnsonBound n 4 k)⌉₊n:ℕk:ℕhkn:k ≤ nthis:Nonempty { s // #s = k } :=
Eq.mpr (id nonempty_subtype._simp_1)
(Eq.mp
(congrArg Exists
(funext fun x =>
Eq.trans mem_powersetCard._simp_1
(Eq.trans (congrArg (fun x_1 => x_1 ∧ #x = k) (subset_univ._simp_1 x)) (true_and (#x = k)))))
(powersetCard_nonempty.mpr (Eq.mpr (id (congrArg (LE.le k) (Fintype.card_fin n))) hkn)))⊢ 0 < ↑α(J(n, k)) n:ℕk:ℕhkn:k ≤ nthis:Nonempty { s // #s = k } :=
Eq.mpr (id nonempty_subtype._simp_1)
(Eq.mp
(congrArg Exists
(funext fun x =>
Eq.trans mem_powersetCard._simp_1
(Eq.trans (congrArg (fun x_1 => x_1 ∧ #x = k) (subset_univ._simp_1 x)) (true_and (#x = k)))))
(powersetCard_nonempty.mpr (Eq.mpr (id (congrArg (LE.le k) (Fintype.card_fin n))) hkn)))⊢ ↑⌈↑(n.choose k) / ↑(johnsonBound n 4 k)⌉₊ ≤ ↑⌈↑(Nat.card { s // #s = k }) / ↑(johnsonBound n 4 k)⌉₊n:ℕk:ℕhkn:k ≤ nthis:Nonempty { s // #s = k } :=
Eq.mpr (id nonempty_subtype._simp_1)
(Eq.mp
(congrArg Exists
(funext fun x =>
Eq.trans mem_powersetCard._simp_1
(Eq.trans (congrArg (fun x_1 => x_1 ∧ #x = k) (subset_univ._simp_1 x)) (true_and (#x = k)))))
(powersetCard_nonempty.mpr (Eq.mpr (id (congrArg (LE.le k) (Fintype.card_fin n))) hkn)))⊢ 0 < ↑α(J(n, k)) All goals completed! 🐙It is known that for $3 \leq k \leq 8$, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.
@[category research solved, AMS 5]
theorem chromaticNumber_johnson_2k_k_lower_bound (hk : 3 ≤ k) (hk' : k ≤ 8) :
k + 1 < J(2 * k, k).chromaticNumber := k:ℕhk:3 ≤ khk':k ≤ 8⊢ ↑k + 1 < χ(J(2 * k, k))
All goals completed! 🐙It is also known that for $3 \leq k \leq 203$ odd, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.
@[category research solved, AMS 5]
theorem chromaticNumber_johnson_2k_k_lower_bound_odd (hk : 3 ≤ k) (hk' : k ≤ 300) (hk_odd : Odd k) :
k + 1 < J(2 * k, k).chromaticNumber := k:ℕhk:3 ≤ khk':k ≤ 300hk_odd:Odd k⊢ ↑k + 1 < χ(J(2 * k, k))
grw [← div_johnsonBound_le_chromaticNum_johnsonk:ℕhk:3 ≤ khk':k ≤ 300hk_odd:Odd k⊢ ↑k + 1 < ↑⌈↑((2 * k).choose k) / ↑(johnsonBound (2 * k) 4 k)⌉₊
All goals completed! 🐙
It can be seen that the chromatic number of $J(2k,k)$ is $>k+1$ for all odd $k>2$.
@[category research solved, AMS 5]
theorem johnson_chromaticNumber_odd (k : ℕ) (hk : 2 < k) (h : Odd k) :
k + 1 < J(2 * k, k).chromaticNumber :=
sorry
Ma and Tang have proved that the chromatic number of $J(2k,k)$ is $>k+1$ for all $k>2$ not of the form $p-1$ for prime $p$.
@[category research solved, AMS 5]
theorem johnson_chromaticNumber_composite (k : ℕ) (hk : 2 < k) (h : (k + 1).Composite) :
k + 1 < J(2 * k, k).chromaticNumber :=
sorry
Ma and Tang's result implies the cases for odd $k$.
@[category test, AMS 5]
theorem johnsonGraph_chromaticNumber_odd_of_johnson_chromaticNumber_composite :
(type_of% johnson_chromaticNumber_composite) → (type_of% johnson_chromaticNumber_odd) := ⊢ (∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < χ(J(2 * k, k))) → ∀ (k : ℕ), 2 < k → Odd k → ↑k + 1 < χ(J(2 * k, k))
intro h h:∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < χ(J(2 * k, k))k:ℕ⊢ 2 < k → Odd k → ↑k + 1 < χ(J(2 * k, k)) h:∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < χ(J(2 * k, k))k:ℕhk:2 < k⊢ Odd k → ↑k + 1 < χ(J(2 * k, k)) h:∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < χ(J(2 * k, k))k:ℕhk:2 < kh_odd:Odd k⊢ ↑k + 1 < χ(J(2 * k, k))
refine h k hk ⟨h:∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < χ(J(2 * k, k))k:ℕhk:2 < kh_odd:Odd k⊢ 1 < k + 1 All goals completed! 🐙, ?_⟩
h:∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < χ(J(2 * k, k))k:ℕhk:2 < kh_odd:Odd k⊢ ∃ m, m ∣ k + 1 ∧ 2 ≤ m ∧ m < k + 1
h:∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < χ(J(2 * k, k))k:ℕhk:2 < kh_odd:Odd k⊢ 2 ∣ k + 1 ∧ 2 ≤ 2 ∧ 2 < k + 1
h:∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < χ(J(2 * k, k))k:ℕhk:2 < kh_odd:Odd k⊢ 2 ∣ k + 1h:∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < χ(J(2 * k, k))k:ℕhk:2 < kh_odd:Odd k⊢ 2 ≤ 2 ∧ 2 < k + 1
h:∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < χ(J(2 * k, k))k:ℕhk:2 < kh_odd:Odd k⊢ 2 ∣ k + 1 All goals completed! 🐙
h:∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < χ(J(2 * k, k))k:ℕhk:2 < kh_odd:Odd k⊢ 2 ≤ 2 ∧ 2 < k + 1 All goals completed! 🐙
Is the chromatic number of J(2 * k, k) always at least k + 2?
@[category research open, AMS 5]
theorem johnson_chromaticNumber : answer(sorry) ↔
∀ k ≥ 3, k + 2 ≤ J(2 * k, k).chromaticNumber :=
sorry
end Erdos835