---

Claim. The answer is yes, with $c=\sqrt{2/\pi}$: the largest family of subsets of $\{1,\ldots,n\}$ in which no member is the union of other members satisfies

$$F(n)\sim\binom{n}{\lfloor n/2\rfloor}\sim\sqrt{\frac{2}{\pi}}\,\frac{2^n}{n^{1/2}}.$$

The argument has two lines. The middle layer, all subsets of size $\lfloor n/2\rfloor$, has no member that is a union of other members, because a union of two or more distinct sets of that size is strictly larger, so $F(n)\ge\binom{n}{\lfloor n/2\rfloor}$. In the other direction, a family with no member a union of other members has in particular no solution of $A\cup B=C$ in distinct members, so it is union-free in the sense of Problem 447, and Kleitman's theorem [Kl71], the solution of that problem, gives $F(n)\le(1+o(1))\binom{n}{\lfloor n/2\rfloor}$. The two bounds match, and Stirling's formula turns the central binomial coefficient into $\sqrt{2/\pi}\,2^n/n^{1/2}$. The printed source of the problem [Er71, item 18] gives the unpublished Erdős–Kleitman bounds and the conjectured asymptotic $\max l_n=(1+o(1))\,c\,2^n/n^{3/2}$ with the exponent $3/2$ in place of $1/2$; the middle layer shows that $3/2$ cannot be right, so the conjecture is false as printed, and the site reads the exponent as a misprint. The claim is the corrected form of the printed conjecture.

Submission note. Posted to the site's forum by Zach Hunter on 13 September 2025:

actually this solves the problem. by problem 447, any such family must have size at most $(1+o(1))\binom{n}{n/2}$. and we still have this as a lower bound.

(The site has been updated to address this comment.)

Depends on. Kleitman 1971, the accepted claim of Problem 447, supplies the upper bound: Kleitman's theorem that a union-free family of subsets of an $n$-set has at most $(1+o(1))\binom{n}{\lfloor n/2\rfloor}$ members.

Claimant. Zach Hunter, posting in the problem's discussion thread on erdosproblems.com under the username zach hunter on 13 September 2025: a first comment gives the middle-layer lower bound and a second, minutes later, the deduction of the upper bound from Problem 447 and the conclusion. The result is a thread observation and not a manuscript; it has a page because it is the result the site credits with the solution.

Acceptance. Reviewed: Thomas Bloom, the site's curator, replied in the thread the same day, thanking both posters and adopting the reading of the exponent in [Er71] as a misprint; the site's problem page labels the problem solved and credits Hunter's observation that the solution of Problem 447 implies $F(n)\sim\binom{n}{n/2}$, which is where the deduction itself is accepted. No refereed publication of the deduction exists; it is two lines over Kleitman's refereed theorem.

Formalization. The Lean file among the links, in Boris Alexeev's repository lean-proofs, declares itself a formalization of a solution to Problem 1023 whose original proof "was found by: Kleitman and Hunter", and says that Kleitman's proof was auto-formalized by Aristotle (Harmonic). It imports the repository's development for Problem 447 (ErdosProblems.Erdos447, Kleitman's theorem as auto-formalized by Aristotle) and uses its erdos_447, the asymptotic $F\sim\binom{n}{\lfloor n/2\rfloor}$ for families with no $A\cup B=C$; a second header block describing the contents of that imported development is carried over into this file. On top of the import it defines a family to be union-free when no member is the join of a nonempty set of other members, the problem's condition, defines $F(n)$ as the largest size of such a family of subsets of an $n$-element type, carries Kleitman's asymptotic over to the problem's families in kleitman_bound_many, identifies the constant as $\sqrt{2/\pi}$ in many_sqrt_two_div_pi, and ends with theorem erdos_1023, the existence of $c>0$ with $F(n)\sim c\,2^n/\sqrt n$, followed by #print axioms whose recorded output lists propext, Classical.choice and Quot.sound. Alexeev announced the file in the thread on 10 February 2026; the link is pinned to the repository's commit of that day. This corpus has not built the file, so the formalization is a link and not formalized evidence. The formal-conjectures statement file for the problem, as of its commit of 18 September 2026, marks it solved and points at the same file of the same repository under a later toolchain folder (v4.29.1), unpinned; a statement file is not a formalization.