FormalConjectures.Wikipedia.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:

Wikipedia

Oeis/A372


namespace DedekindNumber


open Finset


instance piFinBoolDecidableLE {n : ℕ} :
    DecidableRel (fun (a b : Fin n → Bool) => a ≤ b) :=
  fun a b => show Decidable (a ≤ b) from byn:ℕa:Fin n → Boolb:Fin n → Bool⊢ Decidable (a ≤ b)
    rw [Pi.le_def]n:ℕa:Fin n → Boolb:Fin n → Bool⊢ Decidable (∀ (i : Fin n), a i ≤ b i)
    exact Fintype.decidableForallFintypeAll 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 => byn:ℕA:Finset (Finset (Fin n))⊢ Decidable ((fun A => IsSperner A) A)
    unfold IsSperner IsAntichain Set.Pairwisen:ℕ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)
    simp only [Finset.mem_coe, Pi.compl_apply, compl_iff_not]n:ℕA:Finset (Finset (Fin n))⊢ Decidable (∀ ⦃x : Finset (Fin n)⦄, x ∈ A → ∀ ⦃y : Finset (Fin n)⦄, y ∈ A → x ≠ y → ¬x ⊆ y)
    exact inferInstanceAll 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 := by⊢ M 0 = 2 native_decideAll goals completed! 🐙


@[category test, AMS 5]
theorem M_one : M 1 = 3 := by⊢ M 1 = 3 native_decideAll goals completed! 🐙


@[category test, AMS 5]
theorem M_two : M 2 = 6 := by⊢ M 2 = 6 native_decideAll goals completed! 🐙


@[category test, AMS 5]
theorem M_three : M 3 = 20 := by⊢ M 3 = 20 native_decideAll goals completed! 🐙


@[category test, AMS 6]
theorem M'_zero : M' 0 = 2 := by⊢ M' 0 = 2 native_decideAll goals completed! 🐙


@[category test, AMS 6]
theorem M'_one : M' 1 = 3 := by⊢ M' 1 = 3 native_decideAll goals completed! 🐙


@[category test, AMS 6]
theorem M'_two : M' 2 = 6 := by⊢ M' 2 = 6 native_decideAll goals completed! 🐙


@[category test, AMS 6]
theorem M'_three : M' 3 = 20 := by⊢ M' 3 = 20 native_decideAll 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 := byn:ℕv:Fin n → Bool⊢ χ (supp v) = v
  funext ihn:ℕv:Fin n → Booli:Fin n⊢ χ (supp v) i = v i; simp [χ, supp]All goals completed! 🐙


@[category API, AMS 6]
lemma supp_χ {n : ℕ} (s : Finset (Fin n)) : supp (χ s) = s := byn:ℕs:Finset (Fin n)⊢ supp (χ s) = s
  ext ihn:ℕs:Finset (Fin n)i:Fin n⊢ i ∈ supp (χ s) ↔ i ∈ s
  simp [χ, supp]All goals completed! 🐙


@[category API, AMS 6]
lemma χ_le_iff {n : ℕ} (s t : Finset (Fin n)) : χ s ≤ χ t ↔ s ⊆ t := byn:ℕs:Finset (Fin n)t:Finset (Fin n)⊢ χ s ≤ χ t ↔ s ⊆ t
  constructormpn:ℕs:Finset (Fin n)t:Finset (Fin n)⊢ χ s ≤ χ t → s ⊆ tmprn:ℕs:Finset (Fin n)t:Finset (Fin n)⊢ s ⊆ t → χ s ≤ χ t
  ·mpn:ℕs:Finset (Fin n)t:Finset (Fin n)⊢ χ s ≤ χ t → s ⊆ t intro h impn:ℕs:Finset (Fin n)t:Finset (Fin n)h:χ s ≤ χ ti:Fin n⊢ i ∈ s → i ∈ t himpn:ℕs:Finset (Fin n)t:Finset (Fin n)h:χ s ≤ χ ti:Fin nhi:i ∈ s⊢ i ∈ t
    contrapose! hmpn:ℕs:Finset (Fin n)t:Finset (Fin n)i:Fin nhi:i ∈ sh:i ∉ t⊢ ¬χ s ≤ χ t
    exact fun H => byn:ℕs:Finset (Fin n)t:Finset (Fin n)i:Fin nhi:i ∈ sh:i ∉ tH:χ s ≤ χ t⊢ False have := H in:ℕs:Finset (Fin n)t:Finset (Fin n)i:Fin nhi:i ∈ sh:i ∉ tH:χ s ≤ χ tthis:χ s i ≤ χ t i := H i⊢ False; simp_all +decide [ χ ]All goals completed! 🐙
  ·mprn:ℕs:Finset (Fin n)t:Finset (Fin n)⊢ s ⊆ t → χ s ≤ χ t intro h imprn:ℕs:Finset (Fin n)t:Finset (Fin n)h:s ⊆ ti:Fin n⊢ χ s i ≤ χ t i; simp [χ]mprn:ℕs:Finset (Fin n)t:Finset (Fin n)h:s ⊆ ti:Fin n⊢ decide (i ∈ s) ≤ decide (i ∈ t);
    by_cases hi : i ∈ sposn:ℕs:Finset (Fin n)t:Finset (Fin n)h:s ⊆ ti:Fin nhi:i ∈ s⊢ decide (i ∈ s) ≤ decide (i ∈ t)negn:ℕs:Finset (Fin n)t:Finset (Fin n)h:s ⊆ ti:Fin nhi:i ∉ s⊢ decide (i ∈ s) ≤ decide (i ∈ t) <;>posn:ℕs:Finset (Fin n)t:Finset (Fin n)h:s ⊆ ti:Fin nhi:i ∈ s⊢ decide (i ∈ s) ≤ decide (i ∈ t)negn:ℕs:Finset (Fin n)t:Finset (Fin n)h:s ⊆ ti:Fin nhi:i ∉ s⊢ decide (i ∈ s) ≤ decide (i ∈ t) simp_all +decide [ Finset.subset_iff ]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 := byn:ℕv:Fin n → Booli:Fin n⊢ i ∈ supp v ↔ v i = true
  simp [supp]All goals completed! 🐙


@[category API, AMS 6]
lemma toSperner_isSperner {n : ℕ} (f : (Fin n → Bool) → Bool) (_ : Monotone f) :
    IsSperner (toSperner f) := byn:ℕf:(Fin n → Bool) → Boolx✝:Monotone f⊢ IsSperner (toSperner f)
  intro s hsn:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:s ∈ ↑(toSperner f)⊢ ∀ ⦃y : Finset (Fin n)⦄, y ∈ ↑(toSperner f) → s ≠ y → (fun s t => s ⊆ t)ᶜ s y tn:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:s ∈ ↑(toSperner f)t:Finset (Fin n)⊢ t ∈ ↑(toSperner f) → s ≠ t → (fun s t => s ⊆ t)ᶜ s t htn:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:s ∈ ↑(toSperner f)t:Finset (Fin n)ht:t ∈ ↑(toSperner f)⊢ s ≠ t → (fun s t => s ⊆ t)ᶜ s t hstn:ℕ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; simp_all +decide [ Finset.ext_iff]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
  contrapose! hstn:ℕ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; unfold toSperner at *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; aesopAll goals completed! 🐙


@[category API, AMS 6]
lemma fromSperner_monotone {n : ℕ} (A : Finset (Finset (Fin n))) (_ : IsSperner A) :
    Monotone (fromSperner A) := byn:ℕA:Finset (Finset (Fin n))x✝:IsSperner A⊢ Monotone (fromSperner A)
      intro v wn:ℕA:Finset (Finset (Fin n))x✝:IsSperner Av:Fin n → Boolw:Fin n → Bool⊢ v ≤ w → fromSperner A v ≤ fromSperner A w hvwn:ℕA:Finset (Finset (Fin n))x✝:IsSperner Av:Fin n → Boolw:Fin n → Boolhvw:v ≤ w⊢ fromSperner A v ≤ fromSperner A w hfvn:ℕA:Finset (Finset (Fin n))x✝:IsSperner Av:Fin n → Boolw:Fin n → Boolhvw:v ≤ whfv:fromSperner A v = true⊢ fromSperner A w = true
      obtain ⟨s, hsA, hs⟩ : ∃ s ∈ A, s ⊆ supp v := byn:ℕA:Finset (Finset (Fin n))x✝:IsSperner Av:Fin n → Boolw:Fin n → Boolhvw:v ≤ whfv:fromSperner A v = true⊢ ∃ s ∈ A, s ⊆ supp v
        unfold fromSperner at hfvn:ℕA:Finset (Finset (Fin n))x✝:IsSperner Av:Fin n → Boolw:Fin n → Boolhvw:v ≤ whfv:decide (∃ s ∈ A, ∀ i ∈ s, v i = true) = true⊢ ∃ s ∈ A, s ⊆ supp v
        simp_all +decide [ Finset.subset_iff, mem_supp_iff ]All goals completed! 🐙
      have hs_w : s ⊆ supp w := byn:ℕA:Finset (Finset (Fin n))x✝:IsSperner A⊢ Monotone (fromSperner A)
        intro i hin:ℕ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 vi:Fin nhi:i ∈ s⊢ i ∈ supp w; have := hs hin:ℕ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 vi:Fin nhi:i ∈ sthis:i ∈ supp v := hs hi⊢ i ∈ supp w
        simp_all +decide [ Finset.subset_iff, mem_supp_iff ]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 ∈ Ai:Fin nhs:∀ ⦃x : Fin n⦄, x ∈ s → v x = truehi:i ∈ s⊢ w i = true
        exact Bool.eq_false_imp_eq_true.mp fun a ↦ hvw i (hs hi)All goals completed! 🐙
      exact decide_eq_true
        ( ⟨ s, hsA, fun i hi => byn:ℕ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 := 
  fun ⦃i⦄ hi =>
    have this := hs hi;
    Eq.mpr (id (fromSperner_monotone._simp_1 w i))
      (Bool.eq_false_imp_eq_true.mp fun a =>
        hvw i
          (Eq.mp
            (Eq.trans χ_le_iff._simp_1
              (forall_congr fun ⦃x⦄ => implies_congr_ctx (Eq.refl (x ∈ s)) fun a => fromSperner_monotone._simp_1 v x))
            hs hi))i:Fin nhi:i ∈ s⊢ w i = true simpa using Finset.mem_filter.mp ( hs_w hi ) |>.2All goals completed! 🐙 ⟩ )

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

@[category textbook, AMS 5 6]
lemma exists_minimal_true_subset {n : ℕ} {f : (Fin n → Bool) → Bool} (_ : Monotone f)
    {s : Finset (Fin n)} (hs : f (χ s) = true) :
    ∃ t, t ⊆ s ∧ f (χ t) = true ∧ ∀ u, u ⊆ t → f (χ u) = true → t ⊆ u := byn:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:f (χ s) = true⊢ ∃ t ⊆ s, f (χ t) = true ∧ ∀ u ⊆ t, f (χ u) = true → t ⊆ u
      obtain ⟨t, ht₁, ht₂⟩ :
        ∃ t ∈ {t : Finset (Fin n) | t ⊆ s ∧ f (χ t) = true},
        ∀ u ∈ {t : Finset (Fin n) | t ⊆ s ∧ f (χ t) = true}, t.card ≤ u.card := byn:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:f (χ s) = true⊢ ∃ t ∈ {t | t ⊆ s ∧ f (χ t) = true}, ∀ u ∈ {t | t ⊆ s ∧ f (χ t) = true}, #t ≤ #u
        apply_rules [ Set.exists_min_image ]h1n:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:f (χ s) = true⊢ {t | t ⊆ s ∧ f (χ t) = true}.Finitean:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:f (χ s) = true⊢ {t | t ⊆ s ∧ f (χ t) = true}.Nonempty
        ·h1n:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:f (χ s) = true⊢ {t | t ⊆ s ∧ f (χ t) = true}.Finite exact Set.finite_iff_bddAbove.mpr ⟨ s, fun t ht => ht.1 ⟩All goals completed! 🐙
        ·an:ℕf:(Fin n → Bool) → Boolx✝:Monotone fs:Finset (Fin n)hs:f (χ s) = true⊢ {t | t ⊆ s ∧ f (χ t) = true}.Nonempty exact ⟨ s, Finset.Subset.refl _, hs ⟩All goals completed! 🐙
      refine' ⟨ t, ht₁.1, ht₁.2, fun u hu 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) = 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, byn:ℕ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 aesopAll goals completed! 🐙 ⟩ )

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

@[category textbook, AMS 5 6]
lemma fromSperner_toSperner {n : ℕ} (f : (Fin n → Bool) → Bool) (hf : Monotone f) :
    fromSperner (toSperner f) = f := byn:ℕf:(Fin n → Bool) → Boolhf:Monotone f⊢ fromSperner (toSperner f) = f
  funext vhn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Bool⊢ fromSperner (toSperner f) v = f v
  by_cases h : f vposn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = true⊢ fromSperner (toSperner f) v = f vnegn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:¬f v = true⊢ fromSperner (toSperner f) v = f v <;>posn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = true⊢ fromSperner (toSperner f) v = f vnegn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:¬f v = true⊢ fromSperner (toSperner f) v = f v simp_all +decide [ fromSperner ]negn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = false⊢ ∀ x ∈ toSperner f, ∃ x_1 ∈ x, v x_1 = false
  ·posn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = true⊢ ∃ s ∈ toSperner f, ∀ i ∈ s, v i = true obtain ⟨t, ht₁, ht₂⟩ : ∃ t : Finset (Fin n),
    t ⊆ Finset.univ.filter (fun i => v i = true) ∧
    f (χ t) = true ∧
    ∀ u : Finset (Fin n), u ⊆ t → f (χ u) = true → t ⊆ u := byn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = true⊢ ∃ t ⊆ {i | v i = true}, f (χ t) = true ∧ ∀ u ⊆ t, f (χ u) = true → t ⊆ u
      apply exists_minimal_true_subset hfn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = true⊢ f (χ {i | v i = true}) = true;
      convert h using 2h.e'_2.h.e'_1n:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = true⊢ χ {i | v i = true} = v
      exact funext fun i => byn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = truei:Fin n⊢ χ {i | v i = true} i = v i unfold χn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = truei:Fin n⊢ decide (i ∈ {i | v i = true}) = v i; aesopAll goals completed! 🐙;
    exact ⟨ t, Finset.mem_filter.mpr ⟨ Finset.mem_univ _, ht₂.1, ht₂.2 ⟩,
    fun i hi => Finset.mem_filter.mp ( ht₁ hi ) |>.2 ⟩All goals completed! 🐙
  ·negn:ℕf:(Fin n → Bool) → Boolhf:Monotone fv:Fin n → Boolh:f v = false⊢ ∀ x ∈ toSperner f, ∃ x_1 ∈ x, v x_1 = false intro s hsnegn:ℕ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; contrapose! hnegn:ℕ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; simp_all +decide [ toSperner ]negn:ℕ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
    refine' hf _ hs.1negn:ℕ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
    intro inegn:ℕ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; by_cases hi : i ∈ sposn:ℕ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 inegn:ℕ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 <;>posn:ℕ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 inegn:ℕ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 simp_all +decide [ χ ]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 := byn:ℕA:Finset (Finset (Fin n))hA:IsSperner A⊢ toSperner (fromSperner A) = A
  ext shn:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)⊢ s ∈ toSperner (fromSperner A) ↔ s ∈ A; simp [toSperner, fromSperner]hn:ℕ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
  constructorh.mpn:ℕ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 ∈ Ah.mprn:ℕ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 <;>h.mpn:ℕ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 ∈ Ah.mprn:ℕ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 intro hsh.mprn:ℕ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 generalize_proofs at *h.mprn:ℕ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
  ·h.mpn:ℕ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 obtain ⟨ ⟨ t, ht₁, ht₂ ⟩, ht₃ ⟩ := hsh.mpn:ℕ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
    convert ht₁ using 1h.e'_5n:ℕ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 ( byn:ℕ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 unfold χ at 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, decide (i ∈ s) = true⊢ t ⊆ s; aesopAll goals completed! 🐙 ) t ht₁ ( byn:ℕ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 unfold χ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; aesopAll goals completed! 🐙 ) )
      ( byn:ℕ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 unfold χ at 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, decide (i ∈ s) = true⊢ t ⊆ s; aesopAll goals completed! 🐙 )
  ·h.mprn:ℕ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 refine' ⟨ ⟨ s, hs, _ ⟩, _ ⟩h.mpr.refine'_1n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)hs:s ∈ A⊢ ∀ i ∈ s, χ s i = trueh.mpr.refine'_2n:ℕ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 <;>h.mpr.refine'_1n:ℕA:Finset (Finset (Fin n))hA:IsSperner As:Finset (Fin n)hs:s ∈ A⊢ ∀ i ∈ s, χ s i = trueh.mpr.refine'_2n:ℕ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 simp_all +decide [ IsSperner ]h.mpr.refine'_2n:ℕ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
    ·h.mpr.refine'_1n:ℕ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 => byn:ℕ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 unfold χ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; aesopAll goals completed! 🐙
    ·h.mpr.refine'_2n:ℕ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 intro t hth.mpr.refine'_2n:ℕA:Finset (Finset (Fin n))s:Finset (Fin n)hA:IsAntichain (fun s t => s ⊆ t) ↑Ahs:s ∈ At:Finset (Fin n)ht:t ⊆ s⊢ ∀ x ∈ A, (∀ i ∈ x, χ t i = true) → s ⊆ t xh.mpr.refine'_2n:ℕ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)⊢ x ∈ A → (∀ i ∈ x, χ t i = true) → s ⊆ t hxh.mpr.refine'_2n:ℕ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 ∈ A⊢ (∀ i ∈ x, χ t i = true) → s ⊆ t hx'h.mpr.refine'_2n:ℕ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; have := hA hx hsh.mpr.refine'_2n:ℕ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 := hA hx hs⊢ s ⊆ t; simp_all +decide [ Finset.subset_iff, χ ]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' := by⊢ M = M'
  ext nhn:ℕ⊢ M n = M' n
  exact Fintype.card_congr (equivMonotoneSperner 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:= by⊢ kisielewiczFormula 0 = 2 decideAll goals completed! 🐙

@[category test, AMS 5 6] theorem kisielewiczFormula_one : kisielewiczFormula 1 = 3 := by⊢ kisielewiczFormula 1 = 3 decideAll goals completed! 🐙

@[category test, AMS 5 6] theorem kisielewiczFormula_two : kisielewiczFormula 2 = 6 := by⊢ kisielewiczFormula 2 = 6 decideAll goals completed! 🐙

@[category test, AMS 5 6] theorem kisielewiczFormula_three : kisielewiczFormula 3 = 20 := by⊢ kisielewiczFormula 3 = 20
  native_decideAll 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 declaration uses 'sorry'M_eq_kisielewiczFormula : M = kisielewiczFormula := by⊢ M = kisielewiczFormula
  sorryAll goals completed! 🐙

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

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

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

@[category research open, AMS 5 6]
theorem declaration uses 'sorry'Dedekind_10 : M 10 = answer(sorry) := by⊢ M 10 = sorry sorryAll goals completed! 🐙


end DedekindNumber