Skip to content

Erdős problem 497

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

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

497.lean

Retained formal statement1 of 1

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

Sperner's theorem states that F(nn/2)\lvert \mathcal{F}\rvert \leq \binom{n}{\lfloor n/2\rfloor}. This is also known as Dedekind's problem. Resolved by Kleitman [Kl69], who proved that the number of such families is 2(1+o(1))(nn/2).2^{(1+o(1))\binom{n}{\lfloor n/2\rfloor}}.

FormalConjectures/ErdosProblems/497.leanErdos497.erdos_4971 lineExact file
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.

Search problems.science

Find a Problem, Result, source, or page