1. FormalConjectures
  2. Wikipedia
  3. DedekindNumber
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Dedekind Numbers

A Dedekind number M(n) counts the number of monotone Boolean functions on n variables, or equivalently, the number of antichains (Sperner families) in the Boolean lattice 2^[n].

For example, $$M ( 0 ) = 2 , M ( 1 ) = 3 , M ( 2 ) = 6 , and M ( 3 ) = 20 .$$ The first few values grew slowly: $$M ( 4 ) = 168 , M ( 5 ) = 7581$$, but then rapidly: $$M ( 6 ) = 7828354 , M ( 7 ) = 2414682040998 , M ( 8 ) = 56130437228687557907788$$, and $$M ( 9 ) = 286386577668298411128469151667598498812366$$ (computed in 2023).

We formalize two definitions:

    M n: the number of monotone Boolean functions (Fin n → Bool) → Bool

    M' n: the number of antichains (Sperner families) of Finset (Fin n)

We prove their values for small n and show that the two definitions agree for all n.

The problem is to determine the exact values of $M(n)$ for $n ≥ 10$. In particular, the value of $M(10)$ is currently unknown.

References:

namespace DedekindNumberopen Finsetn:ℕa:Fin n → Boolb:Fin n → Bool⊢ Decidable (∀ (i : Fin n), a i ≤ b i) All goals completed! 🐙

$M(n)$ is the number of monotone Boolean functions on $n$ variables.

def M (n : ℕ) : ℕ := Fintype.card {f : (Fin n → Bool) → Bool // Monotone f}

A Sperner family (antichain) of subsets of Fin n: a family of sets such that no member is a subset of another.

def IsSperner {n : ℕ} (A : Finset (Finset (Fin n))) : Prop := IsAntichain (fun s t => s ⊆ t) (A : Set (Finset (Fin n)))instance isSpernerDecidable {n : ℕ} : DecidablePred (fun A : Finset (Finset (Fin n)) => IsSperner A) := fun A => n:ℕA:Finset (Finset (Fin n))⊢ Decidable ((fun A ↦ IsSperner A) A) n:ℕA:Finset (Finset (Fin n))⊢ Decidable ((fun A ↦ ∀ ⦃x : Finset (Fin n)⦄, x ∈ ↑A → ∀ ⦃y : Finset (Fin n)⦄, y ∈ ↑A → x ≠ y → (fun s t ↦ s ⊆ t)ᶜ x y) A) n:ℕA:Finset (Finset (Fin n))⊢ Decidable (∀ ⦃x : Finset (Fin n)⦄, x ∈ A → ∀ ⦃y : Finset (Fin n)⦄, y ∈ A → x ≠ y → ¬x ⊆ y) All goals completed! 🐙

$M'(n)$ is the number of antichains (Sperner families) of subsets of Fin n.

def M' (n : ℕ) : ℕ := Fintype.card {A : Finset (Finset (Fin n)) // IsSperner A}

Values for small n

@[category test, AMS 5] theorem M_zero : M 0 = 2 := ⊢ M 0 = 2 All goals completed! 🐙@[category test, AMS 5] theorem M_one : M 1 = 3 := ⊢ M 1 = 3 All goals completed! 🐙@[category test, AMS 5] theorem M_two : M 2 = 6 := ⊢ M 2 = 6 All goals completed! 🐙@[category test, AMS 5] theorem M_three : M 3 = 20 := ⊢ M 3 = 20 All goals completed! 🐙@[category test, AMS 6] theorem M'_zero : M' 0 = 2 := ⊢ M' 0 = 2 All goals completed! 🐙@[category test, AMS 6] theorem M'_one : M' 1 = 3 := ⊢ M' 1 = 3 All goals completed! 🐙@[category test, AMS 6] theorem M'_two : M' 2 = 6 := ⊢ M' 2 = 6 All goals completed! 🐙@[category test, AMS 6] theorem M'_three : M' 3 = 20 := ⊢ M' 3 = 20 All goals completed! 🐙

The indicator function of a finset: χ s i = true ↔ i ∈ s.

def χ {n : ℕ} (s : Finset (Fin n)) : Fin n → Bool := fun i => decide (i ∈ s)

The support of a Boolean-valued function: supp v = {i | v i = true}.

def supp {n : ℕ} (v : Fin n → Bool) : Finset (Fin n) := univ.filter (fun i => v i = true)

Forward map: monotone function → Sperner family (the minimal true sets).

def toSperner {n : ℕ} (f : (Fin n → Bool) → Bool) : Finset (Finset (Fin n)) := univ.filter (fun s => f (χ s) = true ∧ ∀ t : Finset (Fin n), t ⊆ s → f (χ t) = true → s ⊆ t)

Backward map: Sperner family → monotone Boolean function.

def fromSperner {n : ℕ} (A : Finset (Finset (Fin n))) (v : Fin n → Bool) : Bool := decide (∃ s ∈ A, ∀ i ∈ s, v i = true)/- ### Helper lemmas about χ and supp -/ @[category API, AMS 5] lemma χ_supp {n : ℕ} (v : Fin n → Bool) : χ (supp v) = v := n:ℕv:Fin n → Bool⊢ χ (supp v) = v n:ℕv:Fin n → Booli:Fin n⊢ χ (supp v) i = v i; All goals completed! 🐙@[category API, AMS 6] lemma supp_χ {n : ℕ} (s : Finset (Fin n)) : supp (χ s) = s := n:ℕs:Finset (Fin n)⊢ supp (χ s) = s n:ℕs:Finset (Fin n)i:Fin n⊢ i ∈ supp (χ s) ↔ i ∈ s All goals completed! 🐙@[category API, AMS 6] lemma χ_le_iff {n : ℕ} (s t : Finset (Fin n)) : χ s ≤ χ t ↔ s ⊆ t := n:ℕs:Finset (Fin n)t:Finset (Fin n)⊢ χ s ≤ χ t ↔ s ⊆ t All goals completed! 🐙@[category API, AMS 6] lemma mem_supp_iff {n : ℕ} (v : Fin n → Bool) (i : Fin n) : i ∈ supp v ↔ v i = true := n:ℕv:Fin n → Booli:Fin n⊢ i ∈ supp v ↔ v i = true All goals completed! 🐙@[category API, AMS 6] lemma toSperner_isSperner {n : ℕ} (f : (Fin n → Bool) → Bool) (_ : Monotone f) : IsSperner (toSperner f) := n:ℕf:(Fin n → Bool) → Boolx✝:Monotone f⊢ IsSperner (toSperner f) n:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:s ∈ ↑(toSperner f)t:Finset (Fin n)ht:t ∈ ↑(toSperner f)hst:s ≠ t⊢ (fun s t ↦ s ⊆ t)ᶜ s t; n:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)t:Finset (Fin n)hs:s ∈ toSperner fht:t ∈ toSperner fhst:∃ x, ¬(x ∈ s ↔ x ∈ t)⊢ ¬s ⊆ t n:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)t:Finset (Fin n)hs:s ∈ toSperner fht:t ∈ toSperner fhst:s ⊆ t⊢ ∀ (x : Fin n), x ∈ s ↔ x ∈ t; n:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)t:Finset (Fin n)hs:s ∈ {s | f (χ s) = true ∧ ∀ t ⊆ s, f (χ t) = true → s ⊆ t}ht:t ∈ {s | f (χ s) = true ∧ ∀ t ⊆ s, f (χ t) = true → s ⊆ t}hst:s ⊆ t⊢ ∀ (x : Fin n), x ∈ s ↔ x ∈ t; All goals completed! 🐙n:ℕA:Finset (Finset (Fin n))x✝:IsSperner Av:Fin n → Boolw:Fin n → Boolhvw:v ≤ whfv:fromSperner A v = trues:Finset (Fin n)hsA:s ∈ Ahs:s ⊆ supp vhs_w:s ⊆ supp w⊢ fromSperner A w = true exact decide_eq_true ( ⟨ s, hsA, fun i hi => n:ℕA:Finset (Finset (Fin n))x✝:IsSperner Av:Fin n → Boolw:Fin n → Boolhvw:v ≤ whfv:fromSperner A v = trues:Finset (Fin n)hsA:s ∈ Ahs:s ⊆ supp vhs_w:s ⊆ supp wi:Fin nhi:i ∈ s⊢ w i = true All goals completed! 🐙 ⟩ )

Every true set of a monotone Boolean function contains a minimal true set.

n:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:f (χ s) = truet:Finset (Fin n)ht₁:t ∈ {t | t ⊆ s ∧ f (χ t) = true}ht₂:∀ u ∈ {t | t ⊆ s ∧ f (χ t) = true}, #t ≤ #u⊢ ∃ t ⊆ s, f (χ t) = true ∧ ∀ u ⊆ t, f (χ u) = true → t ⊆ u n:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:f (χ s) = truet:Finset (Fin n)ht₁:t ∈ {t | t ⊆ s ∧ f (χ t) = true}ht₂:∀ u ∈ {t | t ⊆ s ∧ f (χ t) = true}, #t ≤ #uu:Finset (Fin n)hu:u ⊆ thu':f (χ u) = true⊢ t ⊆ u exact Classical.not_not.1 fun h => not_lt_of_ge ( ht₂ u ⟨ hu.trans ht₁.1, hu' ⟩ ) ( Finset.card_lt_card <| Finset.ssubset_iff_subset_ne.2 ⟨ hu, n:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:f (χ s) = truet:Finset (Fin n)ht₁:t ∈ {t | t ⊆ s ∧ f (χ t) = true}ht₂:∀ u ∈ {t | t ⊆ s ∧ f (χ t) = true}, #t ≤ #uu:Finset (Fin n)hu:u ⊆ thu':f (χ u) = trueh:¬t ⊆ u⊢ u ≠ t All goals completed! 🐙 ⟩ )

Converting a monotone function to a Sperner family and back yields the same function.

n:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = truet:Finset (Fin n)ht₁:t ⊆ {i | v i = true}ht₂:f (χ t) = true ∧ ∀ u ⊆ t, f (χ u) = true → t ⊆ u⊢ ∃ s ∈ toSperner f, ∀ i ∈ s, v i = true All goals completed! 🐙 n:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = false⊢ ∀ x ∈ toSperner f, ∃ x_1 ∈ x, v x_1 = false n:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = falses:Finset (Fin n)hs:s ∈ toSperner f⊢ ∃ x ∈ s, v x = false; n:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Bools:Finset (Fin n)hs:s ∈ toSperner fh:∀ x ∈ s, v x ≠ false⊢ f v ≠ false; n:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Bools:Finset (Fin n)hs:f (χ s) = true ∧ ∀ t ⊆ s, f (χ t) = true → s ⊆ th:∀ x ∈ s, v x = true⊢ f v = true n:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Bools:Finset (Fin n)hs:f (χ s) = true ∧ ∀ t ⊆ s, f (χ t) = true → s ⊆ th:∀ x ∈ s, v x = true⊢ χ s ≤ v n:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Bools:Finset (Fin n)hs:f (χ s) = true ∧ ∀ t ⊆ s, f (χ t) = true → s ⊆ th:∀ x ∈ s, v x = truei:Fin n⊢ χ s i ≤ v i; n:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Bools:Finset (Fin n)hs:f (χ s) = true ∧ ∀ t ⊆ s, f (χ t) = true → s ⊆ th:∀ x ∈ s, v x = truei:Fin nhi:i ∈ s⊢ χ s i ≤ v in:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Bools:Finset (Fin n)hs:f (χ s) = true ∧ ∀ t ⊆ s, f (χ t) = true → s ⊆ th:∀ x ∈ s, v x = truei:Fin nhi:i ∉ s⊢ χ s i ≤ v i n:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Bools:Finset (Fin n)hs:f (χ s) = true ∧ ∀ t ⊆ s, f (χ t) = true → s ⊆ th:∀ x ∈ s, v x = truei:Fin nhi:i ∈ s⊢ χ s i ≤ v in:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Bools:Finset (Fin n)hs:f (χ s) = true ∧ ∀ t ⊆ s, f (χ t) = true → s ⊆ th:∀ x ∈ s, v x = truei:Fin nhi:i ∉ s⊢ χ s i ≤ v i All goals completed! 🐙

Converting a Sperner family to a monotone function and back yields the same family.

@[category textbook, AMS 5 6] lemma toSperner_fromSperner {n : ℕ} (A : Finset (Finset (Fin n))) (hA : IsSperner A) : toSperner (fromSperner A) = A := n:ℕA:Finset (Finset (Fin n))hA:IsSperner A⊢ toSperner (fromSperner A) = A n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)⊢ s ∈ toSperner (fromSperner A) ↔ s ∈ A; n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)⊢ ((∃ s_1 ∈ A, ∀ i ∈ s_1, χ s i = true) ∧ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t) ↔ s ∈ A n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)⊢ ((∃ s_1 ∈ A, ∀ i ∈ s_1, χ s i = true) ∧ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t) → s ∈ An:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)⊢ s ∈ A → (∃ s_1 ∈ A, ∀ i ∈ s_1, χ s i = true) ∧ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)⊢ ((∃ s_1 ∈ A, ∀ i ∈ s_1, χ s i = true) ∧ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t) → s ∈ An:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)⊢ s ∈ A → (∃ s_1 ∈ A, ∀ i ∈ s_1, χ s i = true) ∧ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)hs:s ∈ A⊢ (∃ s_1 ∈ A, ∀ i ∈ s_1, χ s i = true) ∧ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t all_goals n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)hs:s ∈ A⊢ (∃ s_1 ∈ A, ∀ i ∈ s_1, χ s i = true) ∧ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)hs:(∃ s_1 ∈ A, ∀ i ∈ s_1, χ s i = true) ∧ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t⊢ s ∈ A n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)ht₃:∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ tt:Finset (Fin n)ht₁:t ∈ Aht₂:∀ i ∈ t, χ s i = true⊢ s ∈ A n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)ht₃:∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ tt:Finset (Fin n)ht₁:t ∈ Aht₂:∀ i ∈ t, χ s i = true⊢ s = t exact subset_antisymm ( ht₃ t ( n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)ht₃:∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ tt:Finset (Fin n)ht₁:t ∈ Aht₂:∀ i ∈ t, χ s i = true⊢ t ⊆ s n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)ht₃:∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ tt:Finset (Fin n)ht₁:t ∈ Aht₂:∀ i ∈ t, decide (i ∈ s) = true⊢ t ⊆ s; All goals completed! 🐙 ) t ht₁ ( n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)ht₃:∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ tt:Finset (Fin n)ht₁:t ∈ Aht₂:∀ i ∈ t, χ s i = true⊢ ∀ i ∈ t, χ t i = true n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)ht₃:∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ tt:Finset (Fin n)ht₁:t ∈ Aht₂:∀ i ∈ t, χ s i = true⊢ ∀ i ∈ t, decide (i ∈ t) = true; All goals completed! 🐙 ) ) ( n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)ht₃:∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ tt:Finset (Fin n)ht₁:t ∈ Aht₂:∀ i ∈ t, χ s i = true⊢ t ⊆ s n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)ht₃:∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ tt:Finset (Fin n)ht₁:t ∈ Aht₂:∀ i ∈ t, decide (i ∈ s) = true⊢ t ⊆ s; All goals completed! 🐙 ) n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)hs:s ∈ A⊢ (∃ s_1 ∈ A, ∀ i ∈ s_1, χ s i = true) ∧ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)hs:s ∈ A⊢ ∀ i ∈ s, χ s i = truen:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)hs:s ∈ A⊢ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)hs:s ∈ A⊢ ∀ i ∈ s, χ s i = truen:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)hs:s ∈ A⊢ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t n:ℕA:Finset (Finset (Fin n))s:Finset (Fin n)hA:IsAntichain (fun s t ↦ s ⊆ t) ↑Ahs:s ∈ A⊢ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t n:ℕA:Finset (Finset (Fin n))s:Finset (Fin n)hA:IsAntichain (fun s t ↦ s ⊆ t) ↑Ahs:s ∈ A⊢ ∀ i ∈ s, χ s i = true exact fun i hi => n:ℕA:Finset (Finset (Fin n))s:Finset (Fin n)hA:IsAntichain (fun s t ↦ s ⊆ t) ↑Ahs:s ∈ Ai:Fin nhi:i ∈ s⊢ χ s i = true n:ℕA:Finset (Finset (Fin n))s:Finset (Fin n)hA:IsAntichain (fun s t ↦ s ⊆ t) ↑Ahs:s ∈ Ai:Fin nhi:i ∈ s⊢ decide (i ∈ s) = true; All goals completed! 🐙 n:ℕA:Finset (Finset (Fin n))s:Finset (Fin n)hA:IsAntichain (fun s t ↦ s ⊆ t) ↑Ahs:s ∈ A⊢ ∀ t ⊆ s, ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t n:ℕA:Finset (Finset (Fin n))s:Finset (Fin n)hA:IsAntichain (fun s t ↦ s ⊆ t) ↑Ahs:s ∈ At:Finset (Fin n)ht:t ⊆ sx:Finset (Fin n)hx:x ∈ Ahx':∀ i ∈ x, χ t i = true⊢ s ⊆ t; n:ℕA:Finset (Finset (Fin n))s:Finset (Fin n)hA:IsAntichain (fun s t ↦ s ⊆ t) ↑Ahs:s ∈ At:Finset (Fin n)ht:t ⊆ sx:Finset (Fin n)hx:x ∈ Ahx':∀ i ∈ x, χ t i = truethis:x ≠ s → (fun s t ↦ s ⊆ t)ᶜ x s⊢ s ⊆ t; All goals completed! 🐙

The set of monotone Boolean functions on n variables is in bijection with the set of Sperner families of subsets of Fin n.

def equivMonotoneSperner (n : ℕ) : {f : (Fin n → Bool) → Bool // Monotone f} ≃ {A : Finset (Finset (Fin n)) // IsSperner A} where toFun := fun ⟨f, hf⟩ => ⟨toSperner f, toSperner_isSperner f hf⟩ invFun := fun ⟨A, hA⟩ => ⟨fromSperner A, fromSperner_monotone A hA⟩ left_inv := fun ⟨f, hf⟩ => Subtype.ext (fromSperner_toSperner f hf) right_inv := fun ⟨A, hA⟩ => Subtype.ext (toSperner_fromSperner A hA)@[category test, AMS 5 6] theorem M_eq_M' : M = M' := ⊢ M = M' n:ℕ⊢ M n = M' n All goals completed! 🐙

A closed formula for the Dedekind numbers as found by Kisielewicz (1998): $$ M(n) = \sum_{k=0}^{2^{2^n}}\prod_{j = 1}^{2 ^ n - 1}\prod_{i = 0}^{j - 1} \left( 1 - b_i^kb_j^k \prod_{m = 0}^{\log_2 i} (1 - b_m^i + b_m^ib_m^j)\right), $$, where $b_i^k$ is the $i$-th bit of $k$.

def kisielewiczFormula (n : ℕ) : ℕ := ∑ k ∈ Finset.range (2 ^ (2 ^ n)), ∏ j ∈ Finset.Icc 1 (2 ^ n), ∏ i ∈ Finset.range j, (1 - (k.testBit i).toNat * (k.testBit j).toNat * ∏ m ∈ Finset.range (i.log2 + 1), (1 - (i.testBit m).toNat + (i.testBit m).toNat * (j.testBit m).toNat))@[category test, AMS 5 6] theorem kisielewiczFormula_zero : kisielewiczFormula 0 = 2:= ⊢ kisielewiczFormula 0 = 2 All goals completed! 🐙@[category test, AMS 5 6] theorem kisielewiczFormula_one : kisielewiczFormula 1 = 3 := ⊢ kisielewiczFormula 1 = 3 All goals completed! 🐙@[category test, AMS 5 6] theorem kisielewiczFormula_two : kisielewiczFormula 2 = 6 := ⊢ kisielewiczFormula 2 = 6 All goals completed! 🐙@[category test, AMS 5 6] theorem kisielewiczFormula_three : kisielewiczFormula 3 = 20 := ⊢ kisielewiczFormula 3 = 20 All goals completed! 🐙

Kisielewicz (1988) proved the following arithmetic formula for the Dedekind numbers: $$ M(n) = \sum_{k=0}^{2^{2^n}}\prod_{j = 1}^{2 ^ n - 1}\prod_{i = 0}^{j - 1} \left( 1 - b_i^kb_j^k \prod_{m = 0}^{\log_2 i} (1 - b_m^i + b_m^ib_m^j)\right), $$ where $b_i^k$ is the $i$-th bit of $k$. However, this formula is not computationally efficient for large $n$.

@[category research solved, AMS 5 6] theorem M_eq_kisielewiczFormula : M = kisielewiczFormula := ⊢ M = kisielewiczFormula All goals completed! 🐙

No closed-form expression that allows efficient computation of Dedekind numbers is currently known.

@[category research open, AMS 5 6] theorem M_eq : M = answer(sorry) := ⊢ M = sorry All goals completed! 🐙

In particular, the Dedekind number for n = 10 is currently unknown.

@[category research open, AMS 5 6] theorem Dedekind_10 : M 10 = answer(sorry) := ⊢ M 10 = sorry All goals completed! 🐙end DedekindNumber