Erdős problem 1022
Is there a constant , where as , such that if is a finite family of finite sets, all of size at least , and for every set there are many with , then has chromatic number (in other words, has property B)?
Sources
FormalConjectures/ErdosProblems/
1022.lean
Retained formal statement
Erdős originally conjectured, in this language, that , which he reports in [Er71] was proved by Lovász.
IsGreatest {c | Erdos1022.SparseImpliesPropertyB 2 c} 1SolvedStatement only, no proof