Erdős problem 1023

Let $F(n)$ be the maximal size of a family of subsets of $\{1,\ldots,n\}$ such that no set in this family is the union of other members of the family. Is it true that there is a constant $c>0$ such that $F(n)\sim c \frac{2^n}{n^{1/2}}?$

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1023.lean

Retained formal statement3 of 3

Hunter observes in the comments that this follows from the solution to [447], which implies $F(n)\sim \binom{n}{n/2}$ .

FormalConjectures/ErdosProblems/1023.leanErdos1023.erdos_1023.variants.hunter1 lineExact file

1Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos1023.F n)) fun n => ↑(n.choose (n / 2))

SolvedStatement only, no proof