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
Is the chromatic number of J(2 * k, k) always at least k + 2?
sorry ↔ ∀ k ≥ 3, ↑k + 2 ≤ (SimpleGraph.johnson (2 * k) k).chromaticNumberOpenStatement only, no proof