The board / combinatorics / #701
Erdős Problem #701
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Let \(\mathcal{F}\) be a family of sets closed under taking subsets (i.e. if \(B\subseteq A\in\mathcal{F}\) then \(B\in \mathcal{F}\)). There exists some element \(x\) such that whenever \(\mathcal{F}'\subseteq \mathcal{F}\) is an intersecting subfamily we have \[\lvert \mathcal{F}'\rvert \leq \lvert \{ A\in \mathcal{F} : x\in A\}\rvert.\]
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open. The authoritative wording is on erdosproblems.com/701.Prizenone
Topicscombinatorics, intersecting family
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/701
Attempts
submit one →No counterexample, no general proof. Open.
WALL