HEXAGONbeta

An Irrationality Measure for Catalan's Constant

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

Contributed by Sean Litsey

Version 1 / Oct 11, 2026 / CC BY 4.0

Abstract

Building on OpenAI's 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 ∣G−a/b∣>b−1 281|G-a/b|>b^{-1\,281} for every integer aa and every sufficiently large integer bb. Thus μ(G)≤1 281\mu(G)\le1\,281; replacing the prime number theorem in the final approximation criterion by Chebyshev's estimates gives 3 6623\,662. We change the determinant parameters, obtaining a 20N20N matrix and a polynomial of degree at most 18N18N. Uniform physical prime-column pools and sparse residue relations sharpen its common denominator. Four exact energy certificates and a separate treatment of free and fixed populations give a uniform mixed-integrand bound. Restricted quadrature and joint atom weights then control the determinant polynomial on ∣x−G∣≤e−120N|x-G|\le e^{-120N}. Prime-index nonvanishing when p2∤bp^2\nmid b completes the measure criterion. We retain the earlier 48N48N construction and its 1 9811\,981 bound to explain the methods. Every ingredient of the new global theorem is formalized in Lean~4 with only the standard axioms and no unproved steps.

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
OpenAI
CodexVersion GPT-6.1 Sol

References

  1. F. Calegari, V. Dimitrov and Y. Tang, The linear independence of 11, ζ(2)\zeta(2), and L(2,χ−3)L(2,\chi_{-3}) , preprint, arXiv:2408.15403 (https://arxiv.org/abs/2408.15403).arXiv
  2. P. Eskandari, Improved rational approximations to Catalan's constant , preprint (2026), arXiv:2609.26354 (https://arxiv.org/abs/2609.26354).arXiv
  3. P. J. Forrester, Meet Andréief, Bordeaux 1886, and Andreev, Kharkov 1882--83 , preprint (2018), arXiv:1806.10411 (https://arxiv.org/abs/1806.10411).arXiv
  4. R. K. Jha, A finite irrationality measure for Catalan'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.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 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), arXiv:2609.04176 (https://arxiv.org/abs/2609.04176).arXiv
  10. D. Wachs, A note on a recent claimed proof of the irrationality of Catalan's constant , preprint (2026), arXiv:2609.22339 (https://arxiv.org/abs/2609.22339).arXiv
Show all 11 referencesShow fewer references
  1. 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 versionSupersededOct 12, 2026
  3. v3Submitted by Sean LitseySubmitted as a new versionCurrentOct 14, 2026