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
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)?
This is false, and for all : a counterexample is provided by Wood [Wo13b], who constructs, for any , a triangle-free -degenerate -uniform hypergraph with chromatic number . A similar counterexample was found independently by KoishiChan in the comments.
This was formalized in Lean by Alexeev using Aristotle.
False ↔ ∃ c, Filter.Tendsto c Filter.atTop Filter.atTop ∧ ∀ (t : ℕ), Erdos1022.SparseImpliesPropertyB t (c t)