Erdős problem 1023 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1023.lean

Retained formal statement1 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_10231 lineExact file

1True ↔ ∃ c, 0 < c ∧ Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(Erdos1023.F n)) fun n => c * 2 ^ n / ↑n ^ (1 / 2)

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science