Source labels openChecked July 26, 2026

Zagier's Conjecture on Multiple Zeta Values

Zagier's conjecture*

Mathematical statement

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$ .

Statement source: Papers statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

zagier_conjecture

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem zagier_conjecture :    answer(sorry) ↔ ∀ n : ℕ, Module.finrank ℚ (mzvSpanOfWeight n) = zagierDim n := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization OEIS A000931background