math.NT — Number Theory

One of β(4), β(6),..., β(36) is irrational

Contributed by Shawn Krisman

Let $\beta(s)=\sum_{m\ge 0}(-1)^m(2m+1)^{-s}$ be Dirichlet's beta function. We prove that at least one of the seventeen numbers $\beta(4),\beta(6),\dots,\beta(36)$ is irrational. All previous explicit results of this kind that we know of include $\beta(2)$, Catalan's constant; our statement does not involve $\beta(2)$ at all. The proof uses the linear forms $L_n=\sum_{t\ge0}(-1)^tR_n''(t)$ attached to a very-well-poised rational function $R_n$ with triple integer zeros and half-integer poles. The second derivative, a $\beta$-analogue of a device of Rivoal, removes $\beta(2)$, and a symmetry removes the odd values. The zeros of $R_n$ run through the region of its poles, which makes every prime $p>n$ harmless. The common denominators are controlled by a $p$-adic analysis and an arithmetic integral that we bound with an exact rational certificate. The size of $L_n$ is bounded by an elementary estimate on the real axis, and its nonvanishing for infinitely many $n$ follows from a saddle-point analysis along a certified contour. The whole proof, including every numerical certificate, has been formalised in Lean 4 with Mathlib and checked by the Lean kernel, using only Lean's three standard axioms.