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
The smallest case not on this page is : But that one can be solved as well: The chromatic number of is at least .
(SimpleGraph.johnson 18 9).chromaticNumber > 9 + 1SolvedStatement only, no proof