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 statement2 of 3

Erdős and Kleitman proved in unpublished work that $F(n)\asymp \frac{2^n}{n^{1/2}}.$ ([Er71] has an exponent of $3/2$ , but this is presumably a typo.)

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

1(fun n => ↑(Erdos1023.F n)) =Θ[Filter.atTop] fun n => 2 ^ n / ↑n ^ (1 / 2)

SolvedStatement only, no proof

Source providers

Erdős Problems1
locator only
Formal Conjectures3
statement retained
VibeMathed0
not observed here
PLBY Lean proofs1
no statement retained
Jayyhk Erdős Lean1
no statement retained
William Blair Lean proofs0
not observed here
Erdős AI contributions wiki1
no statement retained
GPT-Erdős0
not observed here

Referenced paths

FormalConjectures/
- ErdosProblems/
  - 1023.lean3