Lemma 1: $F_n$ is a $\mathbb{Q}$ -linear form in $1, \zeta(r+2), \dots, \zeta(q-2)$ , with denominators (3)

Proved

ZudilinZeta.zudilin_lemma1

by Lucas · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisirrationalitynumber-theoryzeta-values

Lemma 1 of the note. The quantity (2) is a linear form in $1, \zeta(r+2), \zeta(r+4), \dots, \zeta(q-2)$ with rational coefficients; moreover the inclusion

D^r_{m_1 n} D_{m_2 n}\cdots D_{m_{q-r} n}\cdot \Phi_n^{-1}\cdot F_n \in \mathbb{Z} + \mathbb{Z}\zeta(r+2) + \mathbb{Z}\zeta(r+4) + \dots + \mathbb{Z}\zeta(q-2) \tag{3}

holds.

The list $\zeta(r+2), \zeta(r+4), \dots, \zeta(q-2)$ is indexed here as $\zeta(r+2k)$ for $k = 1, \dots, (q-r-2)/2$ ; for the parameters $r = 3$ , $q = 13$ of the note this is exactly $\zeta(5), \zeta(7), \zeta(9), \zeta(11)$ .

Preamble

import Definitions.Def_ZudilinZetaArith

Formal statement

namespace ZudilinZeta
theorem zudilin_lemma1 (P : Params) (n : ℕ) (hn : 0 < n) :
    (∃ c : ℕ → ℚ,
        F P n = (c 0 : ℝ)
          + ∑ k ∈ Finset.Icc 1 ((P.q - P.r - 2) / 2), (c k : ℝ) * zetaR (P.r + 2 * k)) ∧
      (∃ a : ℕ → ℤ,
        Lambda P n = (a 0 : ℝ)
          + ∑ k ∈ Finset.Icc 1 ((P.q - P.r - 2) / 2), (a k : ℝ) * zetaR (P.r + 2 * k)) := by
  sorry
end ZudilinZeta

Source

W. V. Zudilin, One of the numbers ζ(5), ζ(7), ζ(9), ζ(11) is irrational, Uspekhi Mat. Nauk 56:4 (2001), 149–150, https://doi.org/10.4213/rm427 (English transl.: Russian Math. Surveys 56:4 (2001), 774–776)

Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (non-blind: same agent that drafted the statements)

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted the Lean statement, at the human's explicit instruction, and not by an independent blind auditor. Its author had full knowledge of the intended meaning and of the source note, so it cannot corroborate the formalization the way a blind read-back would. A reviewer who wants genuine independent testimony should commission it separately.

The claim is a conjunction, for every P : Params and every natural n with 0 < n.

First conjunct: there exists a function c : ℕ → ℚ such that the real number F P n equals the cast of c 0 plus the sum over k in Finset.Icc 1 ((P.q - P.r - 2) / 2) of c k * zetaR (P.r + 2 * k). Note c is only constrained at the finitely many indices that occur.

Second conjunct: the same with an integer-valued a : ℕ → ℤ in place of c, and with Lambda P n in place of F P n, where Lambda P n is (D (m P 1 * n) ^ P.r * ∏ j in Finset.Icc 2 (P.q - P.r), D (m P j * n)) / Phi P n * F P n.

Both subtractions P.q - P.r - 2 and the division by 2 are natural-number operations, so the index range is 1, …, ⌊(q - r - 2)/2⌋, empty if q < r + 4. The zeta arguments are P.r + 2k, running over r+2, r+4, …. Nothing is asserted about the size of the coefficients, and the statement would be satisfied by any witnesses making the two equalities true.

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 1: FnF_nFn​ is a Q\mathbb{Q}Q-linear form in 1,ζ(r+2),…,ζ(q−2)1, \zeta(r+2), \dots, \zeta(q-2)1,ζ(r+2),…,ζ(q−2), with denominators (3)

Lemma 1: $F_n$ is a $\mathbb{Q}$ -linear form in $1, \zeta(r+2), \dots, \zeta(q-2)$ , with denominators (3)