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}}?$

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1023.lean

Formal Conjectures

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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:1023
PLBY Lean proofsErdosProblems.Erdos1023

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Formalization
Erdős AI contributions wiki · 10 Feb, 2026
Machine
Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science