---

Claim. Let $A(n)$ be the number of antichains in the power set of $[n]$, the families in which no member contains another; it is Dedekind's number, the number of monotone Boolean functions of $n$ variables. Daniel Kleitman proves, in On Dedekind's problem: the number of monotone Boolean functions, that

$$A(n)=2^{(1+o(1))\binom{n}{\lfloor n/2\rfloor}},$$

which answers Problem 497 to the precision Erdős asked for. The lower bound $2^{\binom{n}{\lfloor n/2\rfloor}}$ is immediate, since every subfamily of the middle layer is an antichain, and Sperner's theorem bounds each antichain by that layer's size. Erdős recorded the question, noting that it had been considered before, in his 1961 problem paper (card, section II, item 1), giving the bounds $2^{T_n}<A(n)<\binom{2^n}{T_n}$ with $T_n$ the central binomial coefficient and suggesting that $A(n)<\exp(cT_n)$ with $c$ as close to $\log2$ as desired for large $n$, which is the statement Kleitman proves. Kleitman and Markowsky later sharpened the error term in On Dedekind's problem: the number of isotone Boolean functions. II, Trans. Amer. Math. Soc. 213 (1975), 373–390, recorded here by title only. Neither paper is held here.

Acceptance. Refereed: Proc. Amer. Math. Soc. 21 (1969), no. 3, 677–682; the article's running head dates the issue June 1969 and the page carries the first of that month because the day is not recorded. Reviewed: Thomas Bloom, the site's curator, marks the problem solved and credits the count to Kleitman [Kl69]; the formal-conjectures statement file marks it solved.

Formalizations. One Lean 4 development in Boris Alexeev's lean-proofs collection declares itself a formalization of a solution to this problem with Kleitman as its informal author and Aristotle and Alexeev as its formal authors; its header says it formalizes a write-up titled Counting Antichains in the Boolean Lattice by the graph container method and a supersaturation bound for comparable pairs, a route different from Kleitman's 1969 argument, and it imports the collection's development for Problem 1023. Its final theorem erdos_497 states that $\log_2A(n)$ is asymptotically equivalent to $\binom{n}{\lfloor n/2\rfloor}$. Alexeev announced it on the site's discussion thread on 2026-02-04, and the community database records the Lean qualifier on the site's label from that day; the formal-conjectures statement file points at the copy in that collection. The development was not built or audited here, so the page lists no formalized evidence.