HEXAGONbeta

One of ζ(7),ζ(9),…,ζ(21)\zeta(7),\zeta(9),\dots,\zeta(21) is irrational

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

Contributed by Shawn Krisman ↗

Version 1 / Oct 26, 2026 / CC BY 4.0

Abstract

We prove that at least one of the eight numbers ζ(7),ζ(9),…,ζ(21)\zeta(7),\zeta(9),\dots,\zeta(21) is irrational. The previous best result of this kind not involving ζ(5)\zeta(5), a consequence of a theorem of Lai and Zhou, was that one of ζ(7),…,ζ(35)\zeta(7),\dots,\zeta(35) is irrational. We use Zudilin's hypergeometric construction: sums of fourth derivatives of rational functions with quintuple zeros give linear forms in 1,ζ(7),…,ζ(21)1,\zeta(7),\dots,\zeta(21) with no ζ(3)\zeta(3) or ζ(5)\zeta(5) term. The improvement comes from spreading the poles over eighteen blocks with nearby offsets, a sharper pp-adic bound on the denominators, and a saddle-point analysis of a cotangent contour integral. The estimates rest on exact rational and interval-arithmetic certificates. The whole proof, including these certificates, is formalised in Lean 4 with Mathlib and checked by the Lean kernel using only the standard axioms.

Provenance statement

This was done with a Fable Claude Code session and Opus subsessions.

Tools used

Anthropic
Claude FableVersion 5.1
Anthropic
Claude OpusVersion 5.5

References

  1. Apéry, Roger. Irrationalité de ζ(2)\zeta(2) et ζ(3)\zeta(3). Astérisque, vol. 61, pp. 11–13. 1979
  2. 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
  3. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021DOI
  4. Del Solar, César. ζ(5)\zeta(5) is irrational: a Lean 4 formalization. 2026. Commit 3da8eb1b91f9a90a1c0b7959e845c060dbd16256, 23 September 2026. https://github.com/domino14/zeta5link
  5. 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
  6. Fischler, Stéphane; Sprang, Johannes; Zudilin, Wadim. Many odd zeta values are irrational. Compos. Math., vol. 155, no. 5, pp. 938–952. 2019. arXiv:1803.08905arXivDOI
  7. Kontorovich, Alex; Tao, Terence; others. PrimeNumberTheoremAnd. 2026. Lean project, Apache License 2.0; ported here through the \textttzeta5 repository of C. Del Solar. https://github.com/AlexKontorovich/PrimeNumberTheoremAndlink
  8. Krisman, Shawn. Lean formalisation: one of ζ(7),ζ(9),…,ζ(21)\zeta(7),\zeta(9),\dots,\zeta(21) is irrational. 2026. Tag v1.0. https://github.com/telaviv/zeta-irrationalitylink
  9. Krisman, Shawn. One of β(4),β(6),…,β(36)\beta(4),\beta(6),\dots,\beta(36) is irrational. 2026. Tag v1.0, commit f8df497467901e09fa497553f00d8ffa4480a46d. Manuscript with a Lean 4 formalisation, https://github.com/telaviv/beta-irrationalitylink
  10. 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
Show all 19 referencesShow fewer references
  1. Rivoal, Tanguy. La fonction zêta de Riemann prend une infinité de valeurs irrationnelles aux entiers impairs. C. R. Acad. Sci. Paris Sér. I Math., vol. 331, no. 4, pp. 267–270. 2000. arXiv:math/0008051arXiv
  2. 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
  3. Rivoal, Tanguy; Zudilin, Wadim. A note on odd zeta values. Sém. Lothar. Combin., vol. 81, pp. Art. B81b. 2020. arXiv:1803.03160arXiv
  4. 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
  5. The mathlib Community. mathlib4. 2026. Tag v4.35.0, commit 56a005855ea17e0b0958f73ec801ae140b0a1679. https://github.com/leanprover-community/mathlib4link
  6. Zudilin, Wadim. One of the numbers ζ(5),ζ(7),ζ(9),ζ(11)\zeta(5),\zeta(7),\zeta(9),\zeta(11) is irrational. Russian Math. Surveys, vol. 56, no. 4, pp. 774–776. 2001DOI
  7. Zudilin, Wadim. Irrationality of values of the Riemann zeta function. Izv. Math., vol. 66, no. 3, pp. 489–542. 2002. arXiv:math/0104249arXiv
  8. 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
  9. Zudilin, Wadim. One of the odd zeta values from ζ(5)\zeta(5) to ζ(25)\zeta(25) is irrational. By elementary means. SIGMA Symmetry Integrability Geom. Methods Appl., vol. 14, pp. Paper 028. 2018. arXiv:1801.09895arXiv

Version history

  1. v1Submitted by Shawn KrismanInitial depositCurrentOct 23, 2026