---

Claim. Call a family $\mathcal F$ of subsets of $[n]$ union-free if no three distinct members satisfy $A\cup B=C$, and let $f(n)$ be the largest size of such a family. Daniel Kleitman proves, in Collections of subsets containing no two sets and their union, that

$$f(n)<(1+o(1))\binom{n}{\lfloor n/2\rfloor}.$$

The middle layer of the cube is union-free, so $f(n)$ is asymptotic to the central binomial coefficient. This answers both questions of Problem 447: $f(n)=o(2^n)$, and the bound Erdős hoped for. Erdős stated the problem in his 1961 problem paper (card, section II, item 1), writing that he had long conjectured $l=o(2^n)$, that it would give infinitely many distinct triples $[a_i,a_j]=a_k$ in every sequence of positive density, and adding that $l<(1+o(1))T_n$ with $T_n$ the central binomial coefficient is possible; in 1965 he reported the $o(2^n)$ bound as proved, unpublished, by Sárközy and Szemerédi in the form $c2^n/\log\log n$ (display (69)). The number-theoretic consequence is Problem 487 on the site, and the variant forbidding the union of any number of members is Problem 1023. The paper is not held here; a later note by Kleitman, Extremal properties of collections of subsets containing no two sets and their union, J. Combin. Theory Ser. A 20 (1976), 390–392, is recorded by title only.

Acceptance. Reviewed: Thomas Bloom, the site's curator, marks the problem proved and credits the bound to Kleitman [Kl71]; the formal-conjectures statement file marks both parts solved. The paper appeared in Proc. Sympos. Pure Math. XIX (Combinatorics, 1971), 153–155, an AMS symposium volume rather than a journal, so the page lists no refereed evidence; the record gives only the year, and the page's date is the first day of it.

Formalizations. One Lean 4 development in Boris Alexeev's lean-proofs collection declares itself a formalization of a solution to this problem with Kleitman as its informal author and Aristotle and Alexeev as its formal authors; its header says it formalizes a write-up titled Union-free families and Kleitman's asymptotic bound through the Erdős–Ko–Rado lemma, Kleitman's chain inequality and a linear-programming bound with an explicit dual solution, and its final theorem erdos_447 states that the largest union-free size is asymptotically equivalent to $\binom{n}{\lfloor n/2\rfloor}$. Alexeev announced it on the site's discussion thread on 2026-02-10, and the community database records the Lean qualifier on the site's label from that day; the formal-conjectures statement file points at the copy in that collection. The development was not built or audited here, so the page lists no formalized evidence.