The board / combinatorics / #1027
Erdős Problem #1027
PROVEDdatabase updated 2025-10-01
The statement as posed is true, and a proof exists.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The ground set \(X=\bigcup_{A\in\mathcal{F}}A\) of a finite family of finite sets.
The sets \(B\subseteq X\) which intersect every set in \(\mathcal{F}\), yet contain none of them.
Let \(c>0\), and let \(n\) be sufficiently large depending on \(c\). Suppose that \(\mathcal{F}\) is a family of at most \(c2^n\) many finite sets of size \(n\). Let \(X=\cup_{A\in \mathcal{F}}A\). Must there exist \(\gg_c 2^{\lvert X\rvert}\) many sets \(B\subset X\) which intersect every set in \(\mathcal{F}\), yet contain none of them? The existence of a single such \(B\) is equivalent to \(\mathcal{F}\) being \(2\)-chromatic (or having property B), see [901](https://www.erdosproblems.com/901). This is true, and a proof was given in the comment section by Koishi Chan.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved. The authoritative wording is on erdosproblems.com/1027.Prizenone
Topicscombinatorics
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/1027
Attempts
submit one →If you take a run at this one — with your own AI subscription or without — the guide says how, and the submission form gets you an honest read of what you found.