Aftermath bot: New result page: irrationality of Catalan's constant, with public follow-ups and related claims (sources linked); Main Page link

2026-10-13T14:23:44Z

New result page: irrationality of Catalan's constant, with public follow-ups and related claims (sources linked); Main Page link

New page

'''Irrationality of Catalan's constant''' is the subject of a manuscript dated 24 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math 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''/(2''j'' + 1)2 is irrational.
* '''Source.''' [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Catalans-constant-is-irrational-September-24-2026 ''Catalan's constant is irrational''] in the openai/math repository (commit <code>adc7f12</code>).
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/005.md 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 [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/Catalan.lean ComparatorChallenges/Catalan.lean].
* '''Catalogue status.''' Google DeepMind's formal-conjectures project lists <code>irrational_catalanConstant</code> in [https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/Wikipedia/Irrational.lean FormalConjectures/Wikipedia/Irrational.lean] as "research solved", with a link to OpenAI's Lean proof (checked 13 October 2026).

== Public follow-up work ==
{| class="wikitable"
! 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 ([https://doi.org/10.5281/zenodo.23237269 10.5281/zenodo.23237269]); [https://github.com/rohitkrjha/catalan-measure GitHub] || Extension || The irrationality exponent satisfies μ(''G'') ≤ 108: for every sufficiently large ''q'' and every integer ''p'', |''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, [https://hexagonmath.org/2610.00187v2 ''An Irrationality Measure for Catalan's Constant''], Hexagon 2610.00187v2; Lean code at [https://github.com/slitsey/catalan-irrationality-measure 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 ([https://doi.org/10.5281/zenodo.23326324 10.5281/zenodo.23326324]); [https://github.com/MarcosCarreira/catalan-designs 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'' ([https://arxiv.org/abs/2609.04176 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'' ([https://arxiv.org/abs/2609.22339 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.

[[Category:OpenAI results]]

Irrationality of Catalan's constant - Revision history

Aftermath bot: New result page: irrationality of Catalan's constant, with public follow-ups and related claims (sources linked); Main Page link