HEXAGONbeta

An Irrationality Measure for Catalan's Constant

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

Contributed by Sean Litsey

Version 2 / Oct 11, 2026 / CC BY 4.0

Abstract

uilding on OpenAI's recent proof that Catalan's constant G=∑j≥0(−1)j/(2j+1)2G=\sum_{j\ge0}(-1)^j/(2j+1)^2 is irrational, we prove that \[ \left|G-\frac ab\right|>b^{-8\,127} \] for all integers aa and all sufficiently large integers bb. Thus the irrationality exponent of GG is at most 8 1278\,127; without the prime number theorem in the final step the same argument gives 23 16823\,168. The previous best bound, due to Jha, is 10810^8. The new ingredient is a perturbation estimate for OpenAI's determinant, viewed as a polynomial ΔN(X)\Delta_N(X) in the constant: on the interval ∣x−G∣≤e−404.25N|x-G|\le e^{-404.25N} the polynomial moves by no more than OpenAI's bound for ∣ΔN(G)∣|\Delta_N(G)|. It is proved by a quadrature formula for the coefficient of the constant, an Andr\'eief identity with fixed columns, a generalized Vandermonde bound, and OpenAI's energy method rerun for configurations with fewer points. We also give a new certificate, with re-optimized trial sequences, for one of the two cases of OpenAI's logarithmic-energy dual; it raises the margin of the argument by a factor of almost eight. Every step, including the final theorem, is formalized in Lean~4 on top of OpenAI's formalization, without \texttt{sorry} and with only the standard axioms.

Provenance statement

This work was produced entirely by Claude Opus 5.5 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

References

  1. F. Calegari, V. Dimitrov and Y. Tang, The linear independence of 11, (2) (2), and $L(2,ḩi_ -3 )$ , preprint, https://arxiv.org/abs/2408.15403 arXiv:2408.15403 .arXiv
  2. P. Eskandari, Improved rational approximations to Catalan's constant , preprint (2026), https://arxiv.org/abs/2609.26354 arXiv:2609.26354 .arXiv
  3. P. J. Forrester, Meet Andréief, Bordeaux 1886, and Andreev, Kharkov 1882--83 , preprint (2018), https://arxiv.org/abs/1806.10411 arXiv:1806.10411 .arXiv
  4. R. K. Jha, A finite irrationality measure for Catalan's constant , preprint v1, October 8, 2026, https://doi.org/10.5281/zenodo.23237269 doi:10.5281/zenodo.23237269 ; Lean sources at r̆l https://github.com/rohitkrjha/catalan-measure .DOI
  5. The mathlib Community, The Lean mathematical library , in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 367--381.
  6. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , in: Automated Deduction -- CADE 28, Lecture Notes in Computer Science 12699, Springer, 2021, 625--635.
  7. OpenAI, Catalan's constant is irrational , preprint (September 24, 2026), with a Lean formalization, available at r̆l https://github.com/openai/math (commit fd4aeeb , October 7, 2026).link
  8. T. Rivoal and W. Zudilin, Diophantine properties of numbers related to Catalan's constant , Math. Ann. 326 (2003), 705--721.
  9. Z.-W. Sun, Catalan's constant is irrational , preprint (2026), https://arxiv.org/abs/2609.04176 arXiv:2609.04176 .arXiv
  10. D. Wachs, A note on a recent claimed proof of the irrationality of Catalan's constant , preprint (2026), https://arxiv.org/abs/2609.22339 arXiv:2609.22339 .arXiv
  11. W. Zudilin, An Apéry-like difference equation for Catalan's constant , Electron. J. Combin. 10 (2003), R14.

Version history

  1. v1Submitted by Sean LitseyInitial depositSupersededOct 10, 2026
  2. v2Submitted by Sean LitseySubmitted as a new versionCurrentOct 12, 2026