FormalConjectures.Paper.ZagierMZV

/-
Copyright 2026 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

Zagier's Conjecture on Multiple Zeta Values

References:

[Za94] Zagier, Don. "Values of zeta functions and their applications." First European Congress of Mathematics Paris, July 6–10, 1992: Vol. II: Invited Lectures (Part 2). Basel: Birkhäuser Basel, 1994.

[Co18] Combariza, Germán AG. "A few conjectures about the multiple zeta values." ACM Communications in Computer Algebra 52.1 (2018): 11-20.

[Te02] T. Terasoma. Mixed Tate motives and multiple zeta values. Invent. Math., 149(2):339–369, 2002.

[DG05] P. Deligne and A. Goncharov. Groupes fondamentaux motiviques de Tate mixte. Ann. Sci. Ecole Norm. Sup. (4), 38(1):1–56, 2005.

OEIS A000931


-- TODO(jgd) There are additional conjectures in Co18 which would be nice to formalize.

namespace ZagierMZV


open Finset BigOperators

The multiple zeta value $\zeta(s_1, s_2, \ldots, s_k)$, defined as $$\zeta(s_1, \ldots, s_k) = \sum_{n_1 > n_2 > \cdots > n_k > 0} \frac{1}{n_1^{s_1} n_2^{s_2} \cdots n_k^{s_k}}.$$ The argument is a list of positive natural numbers. The value is well-defined (i.e. the series converges) when the first entry is at least 2, but we define it for all inputs. For the empty list, multiZeta [] = 1 (the empty product convention).

noncomputable def multiZeta : List ℕ → ℝ
  | [] => 1
  | s :: rest => ∑' n : ℕ, (1 / (n + 1 : ℝ) ^ s) * multiZeta.aux rest n
where

Auxiliary function for multiZeta: computes the inner sum $\sum_{n_2 > \cdots > n_k > 0, n_2 < \text{bound}} \frac{1}{n_2^{s_2} \cdots n_k^{s_k}}$.

  aux : List ℕ → ℕ → ℝ
  | [], _ => 1
  | s :: rest, bound => ∑ m ∈ Finset.range bound, (1 / (m + 1 : ℝ) ^ s) * aux rest m

The weight of an MZV index $(s_1, \ldots, s_k)$ is $s_1 + \cdots + s_k$.

def weight (s : List ℕ) : ℕ := s.sum

An MZV index is admissible if it is either empty or if the first entry is at least 2 and all entries are positive. The empty list convention ensures $\mathcal{Z}_0 = \mathbb{Q}$.

def AdmissibleIndex : List ℕ → Prop
  | [] => True
  | s₁ :: rest => 1 < s₁ ∧ ∀ sᵢ ∈ rest, 0 < sᵢ

The set of all MZV values of weight $n$.

def mzvSetOfWeight (n : ℕ) : Set ℝ :=
  multiZeta '' {s | AdmissibleIndex s ∧ weight s = n}

The $\mathbb{Q}$-submodule of $\mathbb{R}$ spanned by all MZVs of weight $n$.

noncomputable def mzvSpanOfWeight (n : ℕ) : Submodule ℚ ℝ :=
  Submodule.span ℚ (mzvSetOfWeight n)

The conjectured Zagier dimension sequence $d_n$, defined by $d_0 = 1$, $d_1 = 0$, $d_2 = 1$, and $d_n = d_{n-2} + d_{n-3}$ for $n \geq 3$.

def zagierDim : ℕ → ℕ
  | 0 => 1
  | 1 => 0
  | 2 => 1
  | (n + 3) => zagierDim (n + 1) + zagierDim n

Zagier's conjecture

The $\mathbb{Q}$-dimension of the vector space spanned by all multiple zeta values of weight $n$ equals $d_n$, where $d_n$ is the Zagier dimension sequence satisfying $d_0 = 1$, $d_1 = 0$, $d_2 = 1$, and $d_n = d_{n-2} + d_{n-3}$ for $n \geq 3$.

@[category research open, AMS 11]
theorem declaration uses 'sorry'zagier_conjecture :
    answer(sorry) ↔ ∀ n : ℕ, Module.finrank ℚ (mzvSpanOfWeight n) = zagierDim n := by⊢ True ↔ ∀ (n : ℕ), Module.finrank ℚ ↥(mzvSpanOfWeight n) = zagierDim n
  sorryAll goals completed! 🐙

Upper bound [Te02, DG05]

The dimension of the $\mathbb{Q}$-vector space of MZVs of weight $n$ is at most $d_n$.

@[category research solved, AMS 11]
theorem declaration uses 'sorry'zagier_upper_bound :
    ∀ n : ℕ, Module.finrank ℚ (mzvSpanOfWeight n) ≤ zagierDim n := by⊢ ∀ (n : ℕ), Module.finrank ℚ ↥(mzvSpanOfWeight n) ≤ zagierDim n
  sorryAll goals completed! 🐙

The first few values of $d_n$ are $1, 0, 1, 1, 1, 2, 2, 3, 4, 5, 7, 9, \ldots$

@[category test, AMS 11]
theorem zagierDim_first_values :
    [zagierDim 0, zagierDim 1, zagierDim 2, zagierDim 3, zagierDim 4,
     zagierDim 5, zagierDim 6, zagierDim 7, zagierDim 8, zagierDim 9] =
    [1, 0, 1, 1, 1, 2, 2, 3, 4, 5] := by⊢ [zagierDim 0, zagierDim 1, zagierDim 2, zagierDim 3, zagierDim 4, zagierDim 5, zagierDim 6, zagierDim 7, zagierDim 8,
    zagierDim 9] =
  [1, 0, 1, 1, 1, 2, 2, 3, 4, 5]
  decideAll goals completed! 🐙

There is no admissible index of weight 1 (since $s_1 \geq 2$ is required).

@[category test, AMS 11]
theorem no_admissible_weight_one (s : List ℕ) (h : AdmissibleIndex s) : weight s ≠ 1 := bys:List ℕh:AdmissibleIndex s⊢ weight s ≠ 1
  cases s with
  | nil =>nilh:AdmissibleIndex []⊢ weight [] ≠ 1
    unfold weightnilh:AdmissibleIndex []⊢ [].sum ≠ 1
    simpAll goals completed! 🐙
  | cons s₁ rest =>conss₁:ℕrest:List ℕh:AdmissibleIndex (s₁ :: rest)⊢ weight (s₁ :: rest) ≠ 1
    unfold weightconss₁:ℕrest:List ℕh:AdmissibleIndex (s₁ :: rest)⊢ (s₁ :: rest).sum ≠ 1
    simp only [List.sum_cons]conss₁:ℕrest:List ℕh:AdmissibleIndex (s₁ :: rest)⊢ s₁ + rest.sum ≠ 1
    unfold AdmissibleIndex at hconss₁:ℕrest:List ℕh:match s₁ :: rest with
| [] => True
| s₁ :: rest => 1 < s₁ ∧ ∀ sᵢ ∈ rest, 0 < sᵢ⊢ s₁ + rest.sum ≠ 1
    obtain ⟨h1, h2⟩ := hconss₁:ℕrest:List ℕh1:1 < s₁h2:∀ sᵢ ∈ rest, 0 < sᵢ⊢ s₁ + rest.sum ≠ 1
    omegaAll goals completed! 🐙

$\mathcal{Z}0 = \mathbb{Q}$, so $\dim\mathbb{Q}(\mathcal{Z}_0) = 1$.

@[category test, AMS 11]
theorem dim_mzv_weight_zero : Module.finrank ℚ (mzvSpanOfWeight 0) = 1 := by⊢ Module.finrank ℚ ↥(mzvSpanOfWeight 0) = 1
  have h_set : mzvSetOfWeight 0 = {1} := by⊢ Module.finrank ℚ ↥(mzvSpanOfWeight 0) = 1
    ext xhx:ℝ⊢ x ∈ mzvSetOfWeight 0 ↔ x ∈ {1}
    simp only [mzvSetOfWeight, Set.mem_image, Set.mem_setOf_eq, Set.mem_singleton_iff]hx:ℝ⊢ (∃ x_1, (AdmissibleIndex x_1 ∧ weight x_1 = 0) ∧ multiZeta x_1 = x) ↔ x = 1
    constructorh.mpx:ℝ⊢ (∃ x_1, (AdmissibleIndex x_1 ∧ weight x_1 = 0) ∧ multiZeta x_1 = x) → x = 1h.mprx:ℝ⊢ x = 1 → ∃ x_1, (AdmissibleIndex x_1 ∧ weight x_1 = 0) ∧ multiZeta x_1 = x
    ·h.mpx:ℝ⊢ (∃ x_1, (AdmissibleIndex x_1 ∧ weight x_1 = 0) ∧ multiZeta x_1 = x) → x = 1 rintro ⟨s, ⟨h_adm, hw⟩, rfl⟩h.mps:List ℕh_adm:AdmissibleIndex shw:weight s = 0⊢ multiZeta s = 1
      cases s with
      | nil =>h.mp.nilh_adm:AdmissibleIndex []hw:weight [] = 0⊢ multiZeta [] = 1
        rflAll goals completed! 🐙
      | cons s₁ rest =>h.mp.conss₁:ℕrest:List ℕh_adm:AdmissibleIndex (s₁ :: rest)hw:weight (s₁ :: rest) = 0⊢ multiZeta (s₁ :: rest) = 1
        unfold weight at hwh.mp.conss₁:ℕrest:List ℕh_adm:AdmissibleIndex (s₁ :: rest)hw:(s₁ :: rest).sum = 0⊢ multiZeta (s₁ :: rest) = 1
        simp only [List.sum_cons] at hwh.mp.conss₁:ℕrest:List ℕh_adm:AdmissibleIndex (s₁ :: rest)hw:s₁ + rest.sum = 0⊢ multiZeta (s₁ :: rest) = 1
        unfold AdmissibleIndex at h_admh.mp.conss₁:ℕrest:List ℕh_adm:match s₁ :: rest with
| [] => True
| s₁ :: rest => 1 < s₁ ∧ ∀ sᵢ ∈ rest, 0 < sᵢhw:s₁ + rest.sum = 0⊢ multiZeta (s₁ :: rest) = 1
        obtain ⟨h1, h2⟩ := h_admh.mp.conss₁:ℕrest:List ℕhw:s₁ + rest.sum = 0h1:1 < s₁h2:∀ sᵢ ∈ rest, 0 < sᵢ⊢ multiZeta (s₁ :: rest) = 1
        omegaAll goals completed! 🐙
    ·h.mprx:ℝ⊢ x = 1 → ∃ x_1, (AdmissibleIndex x_1 ∧ weight x_1 = 0) ∧ multiZeta x_1 = x rintro rflh.mpr⊢ ∃ x, (AdmissibleIndex x ∧ weight x = 0) ∧ multiZeta x = 1
      refine ⟨[], ⟨by⊢ AdmissibleIndex [] simp [AdmissibleIndex]All goals completed! 🐙, by⊢ weight [] = 0 rflAll goals completed! 🐙⟩, by⊢ multiZeta [] = 1 rflAll goals completed! 🐙⟩
  rw [mzvSpanOfWeight, h_set]h_set:mzvSetOfWeight 0 = {1} := 
  Set.ext fun x =>
    Eq.mpr
      (id
        (congr (congrArg Iff (dim_mzv_weight_zero._simp_2 multiZeta {s | AdmissibleIndex s ∧ weight s = 0} x))
          dim_mzv_weight_zero._simp_3))
      {
        mp := fun a =>
          Exists.casesOn a fun s h =>
            And.casesOn h fun left right =>
              And.casesOn left fun h_adm hw =>
                right ▸
                  List.casesOn (motive := fun t => s = t → multiZeta s = 1) s
                    (fun h =>
                      Eq.ndrec (motive := fun s => AdmissibleIndex s → weight s = 0 → multiZeta s = 1)
                        (fun h_adm hw => Eq.refl (multiZeta [])) (Eq.symm h) h_adm hw)
                    (fun s₁ rest h =>
                      Eq.ndrec (motive := fun s => AdmissibleIndex s → weight s = 0 → multiZeta s = 1)
                        (fun h_adm hw =>
                          And.casesOn h_adm fun h1 h2 =>
                            Decidable.byContradiction fun a => dim_mzv_weight_zero._proof_3 s₁ rest hw h1)
                        (Eq.symm h) h_adm hw)
                    (Eq.refl s),
        mpr := fun a => Eq.symm a ▸ Exists.intro [] ⟨⟨True.intro, Eq.refl (weight [])⟩, Eq.refl (multiZeta [])⟩ }⊢ Module.finrank ℚ ↥(ℚ ∙ 1) = 1
  exact finrank_span_singleton (byh_set:mzvSetOfWeight 0 = {1} := 
  Set.ext fun x =>
    Eq.mpr
      (id
        (congr (congrArg Iff (dim_mzv_weight_zero._simp_2 multiZeta {s | AdmissibleIndex s ∧ weight s = 0} x))
          dim_mzv_weight_zero._simp_3))
      {
        mp := fun a =>
          Exists.casesOn a fun s h =>
            And.casesOn h fun left right =>
              And.casesOn left fun h_adm hw =>
                right ▸
                  List.casesOn (motive := fun t => s = t → multiZeta s = 1) s
                    (fun h =>
                      Eq.ndrec (motive := fun s => AdmissibleIndex s → weight s = 0 → multiZeta s = 1)
                        (fun h_adm hw => Eq.refl (multiZeta [])) (Eq.symm h) h_adm hw)
                    (fun s₁ rest h =>
                      Eq.ndrec (motive := fun s => AdmissibleIndex s → weight s = 0 → multiZeta s = 1)
                        (fun h_adm hw =>
                          And.casesOn h_adm fun h1 h2 =>
                            Decidable.byContradiction fun a => dim_mzv_weight_zero._proof_3 s₁ rest hw h1)
                        (Eq.symm h) h_adm hw)
                    (Eq.refl s),
        mpr := fun a => Eq.symm a ▸ Exists.intro [] ⟨⟨True.intro, Eq.refl (weight [])⟩, Eq.refl (multiZeta [])⟩ }⊢ 1 ≠ 0 norm_numAll goals completed! 🐙)

$\mathcal{Z}1 = \emptyset$, so $\dim\mathbb{Q}(\mathcal{Z}_1) = 0$.

@[category test, AMS 11]
theorem dim_mzv_weight_one : Module.finrank ℚ (mzvSpanOfWeight 1) = 0 := by⊢ Module.finrank ℚ ↥(mzvSpanOfWeight 1) = 0
  have h_set : mzvSetOfWeight 1 = ∅ := by⊢ Module.finrank ℚ ↥(mzvSpanOfWeight 1) = 0
    ext xhx:ℝ⊢ x ∈ mzvSetOfWeight 1 ↔ x ∈ ∅
    simp only [mzvSetOfWeight, Set.mem_image, Set.mem_setOf_eq, Set.mem_empty_iff_false]hx:ℝ⊢ (∃ x_1, (AdmissibleIndex x_1 ∧ weight x_1 = 1) ∧ multiZeta x_1 = x) ↔ False
    constructorh.mpx:ℝ⊢ (∃ x_1, (AdmissibleIndex x_1 ∧ weight x_1 = 1) ∧ multiZeta x_1 = x) → Falseh.mprx:ℝ⊢ False → ∃ x_1, (AdmissibleIndex x_1 ∧ weight x_1 = 1) ∧ multiZeta x_1 = x
    ·h.mpx:ℝ⊢ (∃ x_1, (AdmissibleIndex x_1 ∧ weight x_1 = 1) ∧ multiZeta x_1 = x) → False rintro ⟨s, ⟨h_adm, hw⟩, rfl⟩h.mps:List ℕh_adm:AdmissibleIndex shw:weight s = 1⊢ False
      exact no_admissible_weight_one s h_adm hwAll goals completed! 🐙
    ·h.mprx:ℝ⊢ False → ∃ x_1, (AdmissibleIndex x_1 ∧ weight x_1 = 1) ∧ multiZeta x_1 = x rintro hh.mprx:ℝh:False⊢ ∃ x_1, (AdmissibleIndex x_1 ∧ weight x_1 = 1) ∧ multiZeta x_1 = x
      exact h.elimAll goals completed! 🐙
  rw [mzvSpanOfWeight, h_set, Submodule.span_empty, finrank_bot]All goals completed! 🐙


@[category test, AMS 11]
theorem multiZeta_empty : multiZeta [] = 1 := by⊢ multiZeta [] = 1
  simp [multiZeta]All goals completed! 🐙

Euler's identity: $\zeta(2) = \pi^2/6$.

@[category test, AMS 11]
theorem multiZeta_two : multiZeta [2] = Real.pi ^ 2 / 6 := by⊢ multiZeta [2] = Real.pi ^ 2 / 6
  have h1 : multiZeta [2] = ∑' n : ℕ, 1 / (n + 1 : ℝ) ^ 2 := by⊢ multiZeta [2] = Real.pi ^ 2 / 6
    unfold multiZeta⊢ (match [2] with
  | [] => 1
  | s :: rest => ∑' (n : ℕ), 1 / (↑n + 1) ^ s * multiZeta.aux rest n) =
  ∑' (n : ℕ), 1 / (↑n + 1) ^ 2
    simp only [multiZeta.aux, mul_one]All goals completed! 🐙
  rw [h1]h1:multiZeta [2] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2) (funext fun n => mul_one (1 / (↑n + 1) ^ 2)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 2))))⊢ ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 = Real.pi ^ 2 / 6
  have h2 := hasSum_zeta_twoh1:multiZeta [2] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2) (funext fun n => mul_one (1 / (↑n + 1) ^ 2)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 2))))h2:HasSum (fun n => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6) := hasSum_zeta_two⊢ ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 = Real.pi ^ 2 / 6
  have h3 : HasSum (fun n : ℕ => 1 / (n + 1 : ℝ) ^ 2) (Real.pi ^ 2 / 6) := by⊢ multiZeta [2] = Real.pi ^ 2 / 6
    have h4 : (fun n : ℕ => 1 / ((n + 1 : ℕ) : ℝ) ^ 2) = (fun n : ℕ => 1 / (n + 1 : ℝ) ^ 2) := by⊢ multiZeta [2] = Real.pi ^ 2 / 6
      ext nhh1:multiZeta [2] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2) (funext fun n => mul_one (1 / (↑n + 1) ^ 2)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 2))))h2:HasSum (fun n => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6) := hasSum_zeta_twon:ℕ⊢ 1 / ↑(n + 1) ^ 2 = 1 / (↑n + 1) ^ 2
      push_casthh1:multiZeta [2] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2) (funext fun n => mul_one (1 / (↑n + 1) ^ 2)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 2))))h2:HasSum (fun n => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6) := hasSum_zeta_twon:ℕ⊢ 1 / (↑n + 1) ^ 2 = 1 / (↑n + 1) ^ 2
      rflAll goals completed! 🐙
    rw [← h4]h1:multiZeta [2] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2) (funext fun n => mul_one (1 / (↑n + 1) ^ 2)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 2))))h2:HasSum (fun n => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6) := hasSum_zeta_twoh4:(fun n => 1 / ↑(n + 1) ^ 2) = fun n => 1 / (↑n + 1) ^ 2 := 
  funext fun n =>
    Eq.mpr
      (id
        (congrArg (fun x => 1 / x ^ 2 = 1 / (↑n + 1) ^ 2)
          (Eq.trans (Nat.cast_add n 1) (congrArg (HAdd.hAdd ↑n) Nat.cast_one))))
      (Eq.refl (1 / (↑n + 1) ^ 2))⊢ HasSum (fun n => 1 / ↑(n + 1) ^ 2) (Real.pi ^ 2 / 6)
    have := (hasSum_nat_add_iff' 1).mpr h2h1:multiZeta [2] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2) (funext fun n => mul_one (1 / (↑n + 1) ^ 2)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 2))))h2:HasSum (fun n => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6) := hasSum_zeta_twoh4:(fun n => 1 / ↑(n + 1) ^ 2) = fun n => 1 / (↑n + 1) ^ 2 := 
  funext fun n =>
    Eq.mpr
      (id
        (congrArg (fun x => 1 / x ^ 2 = 1 / (↑n + 1) ^ 2)
          (Eq.trans (Nat.cast_add n 1) (congrArg (HAdd.hAdd ↑n) Nat.cast_one))))
      (Eq.refl (1 / (↑n + 1) ^ 2))this:HasSum (fun n => 1 / ↑(n + 1) ^ 2) (Real.pi ^ 2 / 6 - ∑ i ∈ range 1, 1 / ↑i ^ 2) := (hasSum_nat_add_iff' 1).mpr h2⊢ HasSum (fun n => 1 / ↑(n + 1) ^ 2) (Real.pi ^ 2 / 6)
    have h_eval : Real.pi ^ 2 / 6 - ∑ i ∈ range 1, 1 / (i : ℝ) ^ 2 = Real.pi ^ 2 / 6 := by⊢ multiZeta [2] = Real.pi ^ 2 / 6
      simp only [sum_range_one, Nat.cast_zero, zero_pow two_ne_zero, div_zero, sub_zero]All goals completed! 🐙
    rwa [h_eval]h1:multiZeta [2] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 2) (funext fun n => mul_one (1 / (↑n + 1) ^ 2)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 2))))h2:HasSum (fun n => 1 / ↑n ^ 2) (Real.pi ^ 2 / 6) := hasSum_zeta_twoh4:(fun n => 1 / ↑(n + 1) ^ 2) = fun n => 1 / (↑n + 1) ^ 2 := 
  funext fun n =>
    Eq.mpr
      (id
        (congrArg (fun x => 1 / x ^ 2 = 1 / (↑n + 1) ^ 2)
          (Eq.trans (Nat.cast_add n 1) (congrArg (HAdd.hAdd ↑n) Nat.cast_one))))
      (Eq.refl (1 / (↑n + 1) ^ 2))this:HasSum (fun n => 1 / ↑(n + 1) ^ 2) (Real.pi ^ 2 / 6)h_eval:Real.pi ^ 2 / 6 - ∑ i ∈ range 1, 1 / ↑i ^ 2 = Real.pi ^ 2 / 6⊢ HasSum (fun n => 1 / ↑(n + 1) ^ 2) (Real.pi ^ 2 / 6) at this
  exact h3.tsum_eqAll goals completed! 🐙

Euler's identity for $\zeta(4) = \pi^4/90$.

@[category test, AMS 11]
theorem multiZeta_four : multiZeta [4] = Real.pi ^ 4 / 90 := by⊢ multiZeta [4] = Real.pi ^ 4 / 90
  have h1 : multiZeta [4] = ∑' n : ℕ, 1 / (n + 1 : ℝ) ^ 4 := by⊢ multiZeta [4] = Real.pi ^ 4 / 90
    unfold multiZeta⊢ (match [4] with
  | [] => 1
  | s :: rest => ∑' (n : ℕ), 1 / (↑n + 1) ^ s * multiZeta.aux rest n) =
  ∑' (n : ℕ), 1 / (↑n + 1) ^ 4
    simp only [multiZeta.aux, mul_one]All goals completed! 🐙
  rw [h1]h1:multiZeta [4] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4) (funext fun n => mul_one (1 / (↑n + 1) ^ 4)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 4))))⊢ ∑' (n : ℕ), 1 / (↑n + 1) ^ 4 = Real.pi ^ 4 / 90
  have h2 := hasSum_zeta_fourh1:multiZeta [4] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4) (funext fun n => mul_one (1 / (↑n + 1) ^ 4)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 4))))h2:HasSum (fun n => 1 / ↑n ^ 4) (Real.pi ^ 4 / 90) := hasSum_zeta_four⊢ ∑' (n : ℕ), 1 / (↑n + 1) ^ 4 = Real.pi ^ 4 / 90
  have h3 : HasSum (fun n : ℕ => 1 / (n + 1 : ℝ) ^ 4) (Real.pi ^ 4 / 90) := by⊢ multiZeta [4] = Real.pi ^ 4 / 90
    have h4 : (fun n : ℕ => 1 / ((n + 1 : ℕ) : ℝ) ^ 4) = (fun n : ℕ => 1 / (n + 1 : ℝ) ^ 4) := by⊢ multiZeta [4] = Real.pi ^ 4 / 90
      ext nhh1:multiZeta [4] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4) (funext fun n => mul_one (1 / (↑n + 1) ^ 4)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 4))))h2:HasSum (fun n => 1 / ↑n ^ 4) (Real.pi ^ 4 / 90) := hasSum_zeta_fourn:ℕ⊢ 1 / ↑(n + 1) ^ 4 = 1 / (↑n + 1) ^ 4
      push_casthh1:multiZeta [4] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4) (funext fun n => mul_one (1 / (↑n + 1) ^ 4)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 4))))h2:HasSum (fun n => 1 / ↑n ^ 4) (Real.pi ^ 4 / 90) := hasSum_zeta_fourn:ℕ⊢ 1 / (↑n + 1) ^ 4 = 1 / (↑n + 1) ^ 4
      rflAll goals completed! 🐙
    rw [← h4]h1:multiZeta [4] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4) (funext fun n => mul_one (1 / (↑n + 1) ^ 4)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 4))))h2:HasSum (fun n => 1 / ↑n ^ 4) (Real.pi ^ 4 / 90) := hasSum_zeta_fourh4:(fun n => 1 / ↑(n + 1) ^ 4) = fun n => 1 / (↑n + 1) ^ 4 := 
  funext fun n =>
    Eq.mpr
      (id
        (congrArg (fun x => 1 / x ^ 4 = 1 / (↑n + 1) ^ 4)
          (Eq.trans (Nat.cast_add n 1) (congrArg (HAdd.hAdd ↑n) Nat.cast_one))))
      (Eq.refl (1 / (↑n + 1) ^ 4))⊢ HasSum (fun n => 1 / ↑(n + 1) ^ 4) (Real.pi ^ 4 / 90)
    have := (hasSum_nat_add_iff' 1).mpr h2h1:multiZeta [4] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4) (funext fun n => mul_one (1 / (↑n + 1) ^ 4)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 4))))h2:HasSum (fun n => 1 / ↑n ^ 4) (Real.pi ^ 4 / 90) := hasSum_zeta_fourh4:(fun n => 1 / ↑(n + 1) ^ 4) = fun n => 1 / (↑n + 1) ^ 4 := 
  funext fun n =>
    Eq.mpr
      (id
        (congrArg (fun x => 1 / x ^ 4 = 1 / (↑n + 1) ^ 4)
          (Eq.trans (Nat.cast_add n 1) (congrArg (HAdd.hAdd ↑n) Nat.cast_one))))
      (Eq.refl (1 / (↑n + 1) ^ 4))this:HasSum (fun n => 1 / ↑(n + 1) ^ 4) (Real.pi ^ 4 / 90 - ∑ i ∈ range 1, 1 / ↑i ^ 4) := (hasSum_nat_add_iff' 1).mpr h2⊢ HasSum (fun n => 1 / ↑(n + 1) ^ 4) (Real.pi ^ 4 / 90)
    have h_four : 4 ≠ 0 := by⊢ multiZeta [4] = Real.pi ^ 4 / 90 decideAll goals completed! 🐙
    have h_eval : Real.pi ^ 4 / 90 - ∑ i ∈ range 1, 1 / (i : ℝ) ^ 4 = Real.pi ^ 4 / 90 := by⊢ multiZeta [4] = Real.pi ^ 4 / 90
      simp only [sum_range_one, Nat.cast_zero, zero_pow h_four, div_zero, sub_zero]All goals completed! 🐙
    rwa [h_eval]h1:multiZeta [4] = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4 := 
  id
    (of_eq_true
      (Eq.trans (congrArg (fun x => tsum x = ∑' (n : ℕ), 1 / (↑n + 1) ^ 4) (funext fun n => mul_one (1 / (↑n + 1) ^ 4)))
        (eq_self (∑' (n : ℕ), 1 / (↑n + 1) ^ 4))))h2:HasSum (fun n => 1 / ↑n ^ 4) (Real.pi ^ 4 / 90) := hasSum_zeta_fourh4:(fun n => 1 / ↑(n + 1) ^ 4) = fun n => 1 / (↑n + 1) ^ 4 := 
  funext fun n =>
    Eq.mpr
      (id
        (congrArg (fun x => 1 / x ^ 4 = 1 / (↑n + 1) ^ 4)
          (Eq.trans (Nat.cast_add n 1) (congrArg (HAdd.hAdd ↑n) Nat.cast_one))))
      (Eq.refl (1 / (↑n + 1) ^ 4))this:HasSum (fun n => 1 / ↑(n + 1) ^ 4) (Real.pi ^ 4 / 90)h_four:4 ≠ 0h_eval:Real.pi ^ 4 / 90 - ∑ i ∈ range 1, 1 / ↑i ^ 4 = Real.pi ^ 4 / 90⊢ HasSum (fun n => 1 / ↑(n + 1) ^ 4) (Real.pi ^ 4 / 90) at this
  exact h3.tsum_eqAll goals completed! 🐙


end ZagierMZV