The board / combinatorics / #447
Erdős Problem #447
PROVED LEANdatabase updated 2026-02-10
The statement as posed is true, and a proof exists. A solution has also been checked by machine, in Lean.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
The largest size of a union-free collection \(\mathcal{F}\) of subsets of \([n]\).
How large can a union-free collection \(\mathcal{F}\) of subsets of \([n]\) be? By union-free we mean there are no solutions to \(A\cup B=C\) with distinct \(A,B,C\in \mathcal{F}\). Must \(\lvert \mathcal{F}\rvert =o(2^n)\)? In [Er65b] Erdős reported that the estimate \(\lvert \mathcal{F}\rvert=o(2^n)\) was proved in unpublished work by Sárközy and Szemerédi.
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/447.Prizenone
Topicscombinatorics
Statement in LeanFormal Conjectures
Solution in Leanyes
Original pageerdosproblems.com/447
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.