Erdős problem 835
Does there exist a such that the -sized subsets of {1,...,2k} can be coloured with colours such that for every with all colours appear among the -sized subsets of ?
Sources
FormalConjectures/ErdosProblems/
835.lean
Retained formal statement
Ma and Tang's result implies the cases for odd .
(∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumber) → ∀ (k : ℕ), 2 < k → Odd k → ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumberTestStatement only, no proof