HEXAGONbeta

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

Primarily AI-generated textHuman understanding: no partsmath.NT — Number Theory

Contributed by Shawn Krisman

Version 1 / Oct 16, 2026 / CC BY 4.0

Abstract

Let β(s)=∑m≥0(−1)m(2m+1)−s\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 β(4),β(6),…,β(36)\beta(4),\beta(6),\dots,\beta(36) is irrational. All previous explicit results of this kind that we know of include β(2)\beta(2), Catalan's constant; our statement does not involve β(2)\beta(2) at all. The proof uses the linear forms Ln=∑t≥0(−1)tRn′′(t)L_n=\sum_{t\ge0}(-1)^tR_n''(t) attached to a very-well-poised rational function RnR_n with triple integer zeros and half-integer poles. The second derivative, a β\beta-analogue of a device of Rivoal, removes β(2)\beta(2), and a symmetry removes the odd values. The zeros of RnR_n run through the region of its poles, which makes every prime p>np>n harmless. The common denominators are controlled by a pp-adic analysis and an arithmetic integral that we bound with an exact rational certificate. The size of LnL_n is bounded by an elementary estimate on the real axis, and its nonvanishing for infinitely many nn 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.

Provenance statement

This work was produced using two sessions of Opus 5.5. After OpenAI's proof of Catalan's Constant's (β(2)) irrationality we queried Claude to see what we can know about β(4)'s irrationality.

Tools used

Anthropic
Claude OpusVersion 5.5

References

  1. Ball, Keith; Rivoal, Tanguy. Irrationalité d'une infinité de valeurs de la fonction zêta aux entiers impairs. Invent. Math., vol. 146, no. 1, pp. 193–207. 2001DOI
  2. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021DOI
  3. Del Solar, César. ζ(5)\zeta(5) is irrational: a Lean 4 formalization. 2026. Source of the port of the prime number theorem used here (commit 3da8eb1b91f9a90a1c0b7959e845c060dbd16256, 23 September 2026). https://github.com/domino14/zeta5link
  4. NIST Digital Library of Mathematical Functions. F. W. J. Olver, A. B. Olde Daalhuis, D. W. Lozier, B. I. Schneider, R. F. Boisvert, C. W. Clark, B. R. Miller, B. V. Saunders, H. S. Cohl, and M. A. McClain, eds. https://dlmf.nist.gov/, Release 1.2.8 of 2026-09-15link
  5. Fischler, Stéphane. Irrationality of values of LL-functions of Dirichlet characters. J. Lond. Math. Soc. (2), vol. 101, no. 2, pp. 857–876. 2020. arXiv:1904.02402arXivDOI
  6. Kontorovich, Alex; Tao, Terence; others. PrimeNumberTheoremAnd. 2026. Lean project, Apache License 2.0; the formalisation uses files from commit a5154676af9aa3095150ee410cdda80555aa0642 (30 August 2026). https://github.com/AlexKontorovich/PrimeNumberTheoremAndlink
  7. Krisman, Shawn. Lean formalisation: one of β(4),β(6),…,β(36)\beta(4),\beta(6),\dots,\beta(36) is irrational. 2026. Release v1.0, commit f8df497467901e09fa497553f00d8ffa4480a46d. https://github.com/telaviv/beta-irrationalitylink
  8. Lai, Li; Zhou, Li. At least two of ζ(5),ζ(7),…,ζ(35)\zeta(5),\zeta(7),\ldots,\zeta(35) are irrational. Publ. Math. Debrecen, vol. 101, no. 3–4, pp. 353–372. 2022. arXiv:2103.00904arXivDOI
  9. OpenAI. Catalan's constant is irrational. 2026. September 24, 2026. AI-generated and not peer reviewed; Lean formalisation described in \textttlean/docs/005.md of the same repository. OpenAI Math Release preprint, https://github.com/openai/math, file \textttpreprints/Catalans-constant-is-irrational-September-24-2026/paper.pdflink
  10. Rivoal, Tanguy. Irrationalité d'au moins un des neuf nombres ζ(5),ζ(7),…,ζ(21)\zeta(5),\zeta(7),\dots,\zeta(21). Acta Arith., vol. 103, no. 2, pp. 157–167. 2002. arXiv:math/0104221arXivDOI
Show all 15 referencesShow fewer references
  1. Rivoal, Tanguy; Zudilin, Wadim. Diophantine properties of numbers related to Catalan's constant. Math. Ann., vol. 326, no. 4, pp. 705–721. 2003DOI
  2. The mathlib Community. The Lean mathematical library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp. 367–381. 2020. arXiv:1910.09336arXivDOI
  3. The mathlib Community. mathlib4. 2026. Tag v4.35.0, commit 56a005855ea17e0b0958f73ec801ae140b0a1679. https://github.com/leanprover-community/mathlib4link
  4. Zudilin, Wadim. Arithmetic of linear forms involving odd zeta values. J. Théor. Nombres Bordeaux, vol. 16, no. 1, pp. 251–291. 2004. arXiv:math/0206176arXivDOI
  5. Zudilin, Wadim. Arithmetic of Catalan's constant and its relatives. Abh. Math. Semin. Univ. Hambg., vol. 89, no. 1, pp. 45–53. 2019. arXiv:1804.09922arXivDOI

Version history

  1. v1Submitted by Shawn KrismanInitial depositSupersededOct 16, 2026
  2. v2Submitted by Shawn KrismanSubmitted as a new versionCurrentOct 16, 2026