A new upper bound for the irrationality exponent of $ζ(5)$

David Niedbala Giraudin

math.NT Nov 1, 2026 · v1

Read PDF arXiv abstract Code

TL;DR

Relies on a credited third-party Lean 4/Mathlib formalization of Fauzan's ζ(5) irrationality proof, so its hypotheses are machine-checked modulo the prime number theorem.

Abstract

Fauzan's determinantal proof that $ζ(5)$ is irrational also yields $|ζ(5)-a/b|>b^{-260}$ for all large $b$. The exponent is the product $\varrhoλ/\varepsilon$ of three constants attached to the construction, of which $\varrho$ governs the growth of a relative matrix norm. We show that $\varrho$ may be taken to be $9.09$ instead of $6933/500=13.866$, and deduce $|ζ(5)-a/b|>b^{-171}$ for all integers $a$ and all sufficiently large integers $b$, so that the irrationality exponent of $ζ(5)$ is at most $171$. Two closed-form functions replace two worst-case estimates: a node function, which bounds the residue weights individually instead of uniformly, and the external field of the energy estimate, which replaces a factor-by-factor bound on the weight. The result is conditional on Fauzan's preprint. An exact arithmetic verifier is attached.

Problem

Fauzan's determinantal proof that ζ(5) is irrational yields an irrationality exponent bound of 260. The exponent is ϱλ/ε, where ϱ controls the growth of a relative matrix norm ‖B_K‖.

Approach

Two worst-case estimates in Fauzan's Appendix C are replaced by closed-form functions. A node function L(u) bounds each residue weight individually rather than uniformly. The external field V(t) of the energy estimate replaces a factor-by-factor bound on the weight. Combined with a pointwise Legendre-expansion estimate, this gives ϱ = 9.09. An attached Python verifier, using exact rational arithmetic, checks the lemmas and constants. The hypotheses taken from Fauzan's proof are covered by a third-party Lean 4/Mathlib formalization that has no sorry and assumes only θ(x) x.

Results

The relative norm exponent improves from 13.866 to 9.09. This gives |ζ(5) − a/b| > b^{-171} for all sufficiently large b, so the irrationality exponent of ζ(5) is at most 171. The result is conditional on Fauzan's preprint.

K	violations	K^{-1} log\	r_K\
40	0/37	0.55194	0.61286
80	0/74	0.57809	0.61286
120	0/111	0.58799	0.61286
200	0/185	0.59667	0.61286

Check of Lemma 3: worst-case node j=K against L(1)

Papers With

A new upper bound for the irrationality exponent of $ζ(5)$