Erdős problem 497 · problems.science

How many antichains in $[n]$ are there? That is, how many families of subsets of $[n]$ are there such that, if $\mathcal{F}$ is such a family and $A,B\in \mathcal{F}$ , then $A\not\subseteq B$ ?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/497.lean

Formal Conjectures

FormalConjectures/ErdosProblems/497.leanErdos497.erdos_4971 lineExact file

1∃ o, ∃ (_ : o =o[Filter.atTop] 1), ∀ (n : ℕ), ↑(DedekindNumber.M' n) = 2 ^ ((1 + o n) * ↑(n.choose (n / 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:497
PLBY Lean proofsErdosProblems.Erdos497

Reported activity

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

Formalization
Erdős AI contributions wiki · 4 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