HEXAGONbeta

An Irrationality Measure for Catalan's Constant

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

Contributed by Sean Litsey

Version 6 / Oct 11, 2026 / CC BY 4.0

Abstract

Let G=∑j≥0(−1)j(2j+1)−2G=\sum_{j\ge0}(-1)^j(2j+1)^{-2} be Catalan's constant. We prove that ∣G−a/b∣>b−410|G-a/b|>b^{-410} for all integers aa and all sufficiently large integers bb. Hence the irrationality exponent of GG is at most 410410. The proof refines OpenAI's recent proof that GG is irrational. That proof compares two bounds for a large determinant whose entries are linear forms in 11 and GG. The lower bound comes from the denominators of the entries, and the upper bound from an integral representation. We improve both. On the arithmetic side we show that the matrix of rational parts has large corank modulo pp for every prime in an explicit range, which lowers the denominators. On the analytic side we bound a determinant that the energy method treats trivially, using Pick matrices, Heine's formula and an inequality for the logarithmic energy of signed measures. A quadrature formula extends the upper bound to an exponentially small neighbourhood of GG, as a measure requires. The proof is formalized in the Lean proof assistant.

Provenance statement

This work was produced entirely by Claude Opus 5.5, Sonnet 5.5, and Haiku 5.5 running Claude Code and GPT-6.1 Sol running in Codex. This followed a conversation between the human author about why OpenAI's proof of the irrationality of Catalan's constant did not give an irrationality measure.

Tools used

Anthropic
Claude OpusVersion 5.5
Lean
LeanVersion 4
OpenAI
CodexVersion GPT-6.1 Sol
Anthropic
Claude SonnetVersion 5.5
Anthropic
Claude HaikuVersion 5.5
Anthropic
Claude Code

References

  1. Roger Apéry, Irrationalité de ζ(2)\zeta(2) et ζ(3)\zeta(3) , Astérisque 61 (1979), 11--13.
  2. Dmitri I. Arkhipov, Catalan: μ(G)≤528.2327\mu(G)\le528.2327 , GitHub repository, https://github.com/darkhipo/catalan-constant-gen5; verifier submission https://github.com/bigospeedrun/verifier/issues/95, November 1, 2026.link
  3. Frits Beukers, A note on the irrationality of ζ(2)\zeta(2) and ζ(3)\zeta(3) , Bull. London Math. Soc. 11 (1979), no. 3, 268--272.
  4. Hrishik Sai Bojnal, An irrationality exponent below 2402 for C atalan's constant , GitHub repository, October 15, 2026, https://github.com/proof-factory/catalan-exponent; design search and certification by Claude Fable 5.1 (Anthropic), 2026.link
  5. Frank Calegari, Vesselin Dimitrov, and Yunqing Tang, The linear independence of 11 , ζ(2)\zeta(2) , and L(2,χ−3)L(2,\chi_{-3}) , 2024, arXiv:2408.15403 (https://arxiv.org/abs/2408.15403).arXiv
  6. — , Arithmetic holonomy bounds and effective D iophantine approximation , 2025, Theorem 5.1 gives μ(L(2,χ−3))≤24781\mu(L(2,\chi_{-3}))\le 24781, arXiv:2510.04156 (https://arxiv.org/abs/2510.04156).arXiv
  7. Marcos Costa Santos Carreira, Determinant constructions for the D irichlet beta value at four , Preprint, 9 October 2026, doi:10.5281/zenodo.23326647 (https://doi.org/10.5281/zenodo.23326647), 2026.DOI
  8. — , General designs and an irrationality exponent for C atalan's constant , Preprint, 9 October 2026, revised 21 October 2026, doi:10.5281/zenodo.23532239 (https://doi.org/10.5281/zenodo.23532239); sources at https://github.com/MarcosCarreira/catalan-designs, 2026.DOI
  9. Cinna Davis, Catalan's constant: irrationality exponent research , GitHub repository, https://github.com/1337isnot1337/catalan-constant; Lean verification at https://github.com/bigospeedrun/verifier/issues/87, October 31, 2026.link
  10. Leonardo de Moura and Sebastian Ullrich, The L ean 4 theorem prover and programming language , Automated Deduction -- CADE 28, Lecture Notes in Computer Science, vol. 12699, Springer, 2021, pp. 625--635.
Show all 46 referencesShow fewer references
  1. Payman Eskandari, Improved rational approximations to C atalan's constant , 2026, Preprint, 22 September 2026, arXiv:2609.26354 (https://arxiv.org/abs/2609.26354).arXiv
  2. Payman Eskandari, Kumar Murty, and Yusuke Nemoto, Mixed motives and linear forms in the C atalan constant , 2025, Preprint, October 2025 (v3: 29 August 2026), arXiv:2510.20648 (https://arxiv.org/abs/2510.20648).arXiv
  3. Aabir Fauzan, ζ(5)\zeta(5) is irrational , Preprint v1, September 17, 2026, Zenodo, doi:10.5281/zenodo.22826419 (https://doi.org/10.5281/zenodo.22826419), 2026.DOI
  4. Peter J. Forrester, Meet A ndréief, B ordeaux 1886, and A ndreev, K harkov 1882--83 , 2018, arXiv:1806.10411 (https://arxiv.org/abs/1806.10411).arXiv
  5. David Niedbala Giraudin, A new upper bound for the irrationality exponent of ζ(2)\zeta(2) , 2026, Preprint, 2 October 2026, arXiv:2610.02912 (https://arxiv.org/abs/2610.02912).arXiv
  6. — , A new upper bound for the irrationality exponent of ζ(3)\zeta(3) , 2026, Preprint, 22 September 2026, arXiv:2609.26980 (https://arxiv.org/abs/2609.26980).arXiv
  7. Masayoshi Hata, Rational approximations to π\pi and some other numbers , Acta Arith. 63 (1993), no. 4, 335--349.
  8. R. K. Jha, A finite irrationality measure for C atalan's constant , Preprint v1, October 8, 2026, doi:10.5281/zenodo.23237269 (https://doi.org/10.5281/zenodo.23237269); Lean sources at https://github.com/rohitkrjha/catalan-measure, 2026.DOI
  9. Fredrik Johansson, Arb: efficient arbitrary-precision midpoint-radius interval arithmetic , IEEE Trans. Comput. 66 (2017), no. 8, 1281--1292, arXiv:1611.02831 (https://arxiv.org/abs/1611.02831).arXiv
  10. Christian Krattenthaler and Tanguy Rivoal, On a linear form for C atalan's constant , South East Asian J. Math. Math. Sci. 6 (2008), no. 2, 3--15, arXiv:0810.1927 (https://arxiv.org/abs/0810.1927).arXiv
  11. Christian Krattenthaler and Wadim Zudilin, Hypergeometry inspired by irrationality questions , Kyushu J. Math. 73 (2019), no. 1, 189--203, arXiv:1802.08856 (https://arxiv.org/abs/1802.08856).arXiv
  12. Li Lai, The linear independence of 11 , ζ(3)\zeta(3) , and ζ(4)\zeta(4) , 2026, Preprint, 5 October 2026 (v2: 15 October 2026), arXiv:2610.06838 (https://arxiv.org/abs/2610.06838).arXiv
  13. Lean FRO , Comparator: checking a L ean proof against a trusted statement , https://github.com/leanprover/comparator, 2026, Software; accessed October 2026.link
  14. Elyasheev Leibtag, Hila Barkan, Rotem Kalisch, Shachar Weinbaum, Michael Shalyt, and Ido Kaminer, New directions in irrationality , 2026, Preprint, 20 October 2026, arXiv:2610.27799 (https://arxiv.org/abs/2610.27799); supplement and code at https://github.com/RamanujanMachine/new-directions-in-irrationality.arXiv
  15. Sean Litsey, Irrationality measures for L(2,χ−3)L(2,\chi_{-3}) and other differences of trigamma values , Hexagon preprint hexagon:2610.00401, https://hexagonmath.org/2610.00401, 2026.hexagon
  16. Jingwen Liu, Kai Jiang, and Pingwen Zhang, Irrationality exponents of logarithms of positive rational numbers , 2026, Preprint, 7 October 2026, revised 8 October 2026 (v2), arXiv:2610.10192 (https://arxiv.org/abs/2610.10192).arXiv
  17. Raffaele Marcovecchio, The R hin-- V iola method for log⁡2\log 2 , Acta Arith. 139 (2009), no. 2, 147--184.
  18. OpenAI , Catalan's constant is irrational , Preprint dated September 24, 2026, released October 6, 2026, with a Lean formalization, available at the original paper PDF (https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Catalans-constant-is-irrational-September-24-2026/paper.pdf) and the Lean formalization (https://github.com/openai/math/tree/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/OAI/NumberTheory/Catalan) (repository commit fd4aeeb , October 7, 2026), 2026.link
  19. — , The irrationality exponent of π\pi is 2 , Preprint dated September 24, 2026, released October 6, 2026, https://github.com/openai/math/tree/main/preprints/The-irrationality-exponent-of-pi-is-2-September-24-2026, 2026.link
  20. Thomas Prellberg, Three irrationality results for the dilogarithm: R hin-- V iola and V iola-- Z udilin constructions at −1/4-1/4 , 1/51/5 , and −1/3-1/3 , 2026, Preprint, 7 September 2026, arXiv:2609.06895 (https://arxiv.org/abs/2609.06895).arXiv
  21. Georges Rhin and Carlo Viola, On a permutation group related to ζ(2)\zeta(2) , Acta Arith. 77 (1996), no. 1, 23--56.
  22. — , The group structure for ζ(3)\zeta(3) , Acta Arith. 97 (2001), no. 3, 269--293.
  23. Tanguy Rivoal and Wadim Zudilin, Diophantine properties of numbers related to C atalan's constant , Math. Ann. 326 (2003), no. 4, 705--721.
  24. Edward B. Saff and Vilmos Totik, Logarithmic potentials with external fields , Grundlehren der mathematischen Wissenschaften, vol. 316, Springer, Berlin, 1997.
  25. V. Kh. Salikhov, On the irrationality measure of the number π\pi , Russian Math. Surveys 63 (2008), no. 3, 570--572.
  26. Zhi-Wei Sun, Catalan's constant is irrational , 2026, arXiv:2609.04176 (https://arxiv.org/abs/2609.04176).arXiv
  27. The mathlib Community , The L ean mathematical library , Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 2020, pp. 367--381.
  28. The PrimeNumberTheoremAnd contributors , The PNT+ project: a L ean formalization of the prime number theorem and related results , https://github.com/AlexKontorovich/PrimeNumberTheoremAnd, The vendored compatibility additions used here are recorded in the repository's NOTICE and PORTING.md .link
  29. Dane Wachs, A note on a recent claimed proof of the irrationality of C atalan's constant , 2026, arXiv:2609.22339 (https://arxiv.org/abs/2609.22339).arXiv
  30. Ryan Xu, Improved κ=2\kappa=2 trial: μ(G)≤727.03\mu(G)\le727.03 , GitHub issue, October 22, 2026, https://github.com/slitsey/catalan-irrationality-measure/issues/5; data and scripts at https://github.com/ry-xu/slightlysupervised, 2026.link
  31. Doron Zeilberger and Wadim Zudilin, The irrationality measure of π\pi is at most 7.103205334137…7.103205334137\ldots , Mosc. J. Comb. Number Theory 9 (2020), no. 4, 407--419, arXiv:1912.06345 (https://arxiv.org/abs/1912.06345).arXiv
  32. Wadim Zudilin, A few remarks on linear forms involving C atalan's constant , Chebyshevskii Sb. 3 (2002), no. 2(4), 60--70, In Russian, arXiv:math/0210423 (https://arxiv.org/abs/math/0210423).arXiv
  33. — , An A péry-like difference equation for C atalan's constant , Electron. J. Combin. 10 (2003), Research Paper 14, arXiv:math/0201024 (https://arxiv.org/abs/math/0201024).arXiv
  34. — , Two hypergeometric tales and a new irrationality measure of ζ(2)\zeta(2) , Ann. Math. Québec 38 (2014), no. 1, 101--117, arXiv:1310.1526 (https://arxiv.org/abs/1310.1526).arXiv
  35. — , A determinantal approach to irrationality , Constr. Approx. 45 (2017), no. 2, 301--310, arXiv:1507.05697 (https://arxiv.org/abs/1507.05697).arXiv
  36. — , Arithmetic of C atalan's constant and its relatives , Abh. Math. Semin. Univ. Hambg. 89 (2019), no. 1, 45--53, arXiv:1804.09922 (https://arxiv.org/abs/1804.09922).arXiv

Version history

  1. v1Submitted by Sean LitseyInitial depositSupersededOct 10, 2026
  2. v2Submitted by Sean LitseySubmitted as a new versionSupersededOct 12, 2026
  3. v3Submitted by Sean LitseySubmitted as a new versionSupersededOct 14, 2026
  4. v4Submitted by Sean LitseySubmitted as a new versionSupersededOct 16, 2026
  5. v5Submitted by Sean LitseySubmitted as a new versionSupersededOct 18, 2026
  6. v6Submitted by Sean LitseySubmitted as a new versionCurrentNov 03, 2026