Skip to content

Erdős problem 1022

Is there a constant ctc_t, where ctc_t\to \infty as tt\to \infty, such that if F\mathcal{F} is a finite family of finite sets, all of size at least tt, and for every set XX there are <ctX<c_t\lvert X\rvert many AFA\in \mathcal{F} with AXA\subseteq X, then F\mathcal{F} has chromatic number 22 (in other words, has property B)?

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1022.lean

Retained formal statement1 of 3

Is there a constant ctc_t, where ctc_t\to \infty as tt\to \infty, such that if F\mathcal{F} is a finite family of finite sets, all of size at least tt, and for every set XX there are <ctX<c_t\lvert X\rvert many AFA\in \mathcal{F} with AXA\subseteq X, then F\mathcal{F} has chromatic number 22 (in other words, has property B)?

This is false, and ct<2c_t<2 for all tt: a counterexample is provided by Wood [Wo13b], who constructs, for any r2r\geq 2, a triangle-free 22-degenerate rr-uniform hypergraph with chromatic number 33. A similar counterexample was found independently by KoishiChan in the comments.

This was formalized in Lean by Alexeev using Aristotle.

FormalConjectures/ErdosProblems/1022.leanErdos1022.erdos_10221 lineExact file
False ↔ ∃ c, Filter.Tendsto c Filter.atTop Filter.atTop ∧ ∀ (t : ℕ), Erdos1022.SparseImpliesPropertyB t (c t)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page