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
Johnson's bound for the chromatic number of the Johnson graph.
∀ {n k : ℕ}, ↑⌈↑(n.choose k) / ↑(Erdos835.johnsonBound n 4 k)⌉₊ ≤ (SimpleGraph.johnson n k).chromaticNumberSolvedStatement only, no proof