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
It is also known that for odd, the chromatic number of is greater than , see [Johnson graphs](https://aeb.win.tue.nl/graphs/Johnson.html).
∀ {k : ℕ}, 3 ≤ k → k ≤ 300 → Odd k → ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumberSolvedStatement only, no proof