Irrationality of Catalan's constant
Irrationality of Catalan's constant is the subject of a manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original result
- Claim. Catalan's constant G = ∑j≥0 (−1)j/(2j + 1)2 is irrational.
- Source. Catalan's constant is irrational in the openai/math repository (commit
adc7f12). - Formalization, as described by the repository. The scope note lean/docs/005.md states that the Lean formalization proves that G is irrational, the assertion in the paper's title; the comparator statement is ComparatorChallenges/Catalan.lean.
- Catalogue status. Google DeepMind's formal-conjectures project lists
irrational_catalanConstantin FormalConjectures/Wikipedia/Irrational.lean as "research solved", with a link to OpenAI's Lean proof (checked 13 October 2026).
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 13 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | R. K. Jha, A finite irrationality measure for Catalan's constant, Zenodo (10.5281/zenodo.23237269); GitHub | Extension | G − p/q| > q−100,000,000. The proof extends OpenAI's determinant proof by bounding every complementary minor. | The record states that the bound and its supporting estimates are formalized in Lean, and includes the manuscript, its sources and the Lean project. |
| 2026-10-10 (v1); v2 2026-10-11 | S. Litsey, An Irrationality Measure for Catalan's Constant, Hexagon 2610.00187v2; Lean code at slitsey/catalan-irrationality-measure | Extension | G − a/b| > b−8127 for all integers a and all sufficiently large b, so μ(G) ≤ 8127 (23,168 without the prime number theorem in the final step). The new ingredient is a perturbation estimate for OpenAI's determinant viewed as a polynomial in the constant. | Posted on Hexagon (v2). The page states "This work was produced entirely by Claude Opus 5.5", with human understanding of "no parts". The GitHub repository contains a Lean 4 formalization building on OpenAI's. |
| 2026-10-12 | M. C. S. Carreira, General designs and an irrationality exponent for Catalan's constant, Zenodo (10.5281/zenodo.23326324); GitHub | Extension | States four conditions on the five design parameters under which OpenAI's argument goes through unchanged, and exhibits a second design with a certified gap of about 0.0026 (the original gap is about 0.00013). For it, an upper bound below 2715 for the irrationality exponent, using Jha's ingredients and Litsey's degree bound. A companion note reports attempts on the Dirichlet beta value β(4). | The record states that the note was prepared with the assistance of Claude, that all computations were run by the author, and that it has not been refereed; scripts and run logs are public. |
Related claims
- Z.-W. Sun, Catalan's constant is irrational (arXiv:2609.04176, v1, 3 September 2026), claims a proof by a different method, using weighted tails of the series.
- D. Wachs, A note on a recent claimed proof of the irrationality of Catalan's constant (arXiv:2609.22339, v1, 16 September 2026), reports exact computations showing that "the published derivation does not justify the claimed estimate, so the proof of the main theorem is incomplete", and states that nothing is concluded about the irrationality of G.
Notes
- The follow-ups state AI assistance as recorded in the table.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.