Riemann Zeta Function zeta(5)

is the value of the Riemann zeta function at 5, given by

(OEIS A013663).

A binomial sum identity is

where is a binomial coefficient and is a generalized harmonic number (Borwein and Bradley 1996).

Rapidly converging series include

(Plouffe 1998). Related series are

(Plouffe 2006).

Huvent (2002) gave the series

where is a harmonic number. A sum limit is

(Apostol 1973, given incorrectly in Stark 1974), where tends to infinity through positive integers.

The derivative of the Riemann zeta function satisfies

Fauzan (2026) announced a proof that is irrational. The construction uses rationally normalized determinants of Hankel matrices to produce integer polynomials of degree satisfying

for all sufficiently large positive integers . A moment representation with a positive weight proves that these determinants do not vanish at . An analytic estimate bounds their values, while local arithmetic estimates ensure integer coefficients after normalization and preserve the required decay.

To obtain a proof by contradiction, suppose with an integer and a positive integer. Since is an integer polynomial of degree , the number is an integer and satisfies

For fixed , the right-hand side tends to zero as , contradicting the fact that a positive integer is at least 1.

Fauzan (2026) also reports the bound

for every integer and all sufficiently large positive integer denominators . The irrationality measure of therefore satisfies

Lean implementations of the proof are available with different assumptions and estimates. Romik (2026) reports a formal verification that is irrational, assuming the prime number theorem as an additional axiom. The Zeta5 project (mo271 2026) uses a formalized prime number theorem and reports that the final theorem depends only on the standard logical axioms used by Lean. Its normalizing factor and local estimates differ from those in Fauzan (2026), and its decay estimate suffices to prove that is irrational without reproducing the constant above.