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 2 / 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.

Author comments: Updated the paper to acknowledge that this result was found by CoolRmal several weeks earlier.

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. CoolRmal. Irrationality of odd zeta values: one of ζ(7),…,ζ(21)\zeta(7),\dots,\zeta(21), a Lean 4 formalization. 2026. Formalisation completed 29 September 2026; unrefereed. https://github.com/CoolRmal/odd-zeta-irrationalitylink
  4. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021DOI
  5. Del Solar, César. ζ(5)\zeta(5) is irrational: a Lean 4 formalization. 2026. Commit 3da8eb1b91f9a90a1c0b7959e845c060dbd16256, 23 September 2026. https://github.com/domino14/zeta5link
  6. 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
  7. 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
  8. 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
  9. 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
  10. 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
Show all 21 referencesShow fewer references
  1. 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
  2. Liu, Jingwei. At least one of ζ(7),ζ(9),…,ζ(19)\zeta(7), \zeta(9), \dots, \zeta(19) is irrational: a growing-determinant proof with Lean certification. 2026. Version 1.0.0, 6 October 2026; unrefereed. Zenodo, https://doi.org/10.5281/zenodo.23191331; code at https://github.com/AlexxxxxLiu/odd-zeta-seven-leanlink
  3. 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
  4. 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
  5. Rivoal, Tanguy; Zudilin, Wadim. A note on odd zeta values. Sém. Lothar. Combin., vol. 81, pp. Art. B81b. 2020. arXiv:1803.03160arXiv
  6. 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
  7. The mathlib Community. mathlib4. 2026. Tag v4.35.0, commit 56a005855ea17e0b0958f73ec801ae140b0a1679. https://github.com/leanprover-community/mathlib4link
  8. 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
  9. Zudilin, Wadim. Irrationality of values of the Riemann zeta function. Izv. Math., vol. 66, no. 3, pp. 489–542. 2002. arXiv:math/0104249arXiv
  10. 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
  11. 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. v1 · 34 pagesSubmitted by Shawn KrismanInitial depositSupersededOct 23, 2026
  2. v2 · 34 pagesSubmitted by Shawn KrismanUpdated the paper to acknowledge that this result was found by CoolRmal several weeks earlier.CurrentNov 11, 2026