---
id: "2026-10-06-openai-catalan-constant-irrational"
url: "https://postcutoff.com/e/2026-10-06-openai-catalan-constant-irrational/"
as_of: "2026-10-30T13:42:00+01:00"
date: "2026-10-06"
date_precision: day
category: science
importance: 5
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 8
editor: human editor
human_review: null
version: "2026-10-29"
---

As of: 2026-10-30 13:42 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-06-openai-catalan-constant-irrational/

# OpenAI: Catalan's constant is irrational (Lean)

Full title: OpenAI's release proves Catalan's constant is irrational, with a Lean proof of the exact statement

"Catalan's constant is irrational" (OpenAI, 24 Sep 2026, released 6 Oct, family 005) proves Theorem 1.1, "Catalan's constant is irrational", for G = Σ (−1)^j/(2j+1)² = β(2) = L(2, χ₋₄). Earlier results only showed that some value among β(2), β(4), …, β(10) is irrational. The proof builds large determinants from moments that are rational combinations of 1, G and ζ(2), cancels the ζ(2) part, and plays denominator bounds against analytic bounds, with nonvanishing certified by a finite computation. The main theorem is formalized in Lean and the comparator check passed; no expert has yet published a full human reading. Follow-ups derive irrationality measures such as μ(G) ≤ 740.

## Key facts
- Paper: 'Catalan's constant is irrational' (OpenAI, 44 pp., dated 24 Sep 2026). Abstract (verbatim): 'We prove that Catalan’s constant G = Σ_{j≥0} (−1)^j/(2j + 1)² is irrational.'
- Prior state (paper, §1.1): Rivoal and Zudilin proved that infinitely many even beta values are irrational and that one of β(2), …, β(14) is; Zudilin reduced this to β(12) and Lai–Zhou to β(10). 'Such family results guarantee irrational members without identifying the particular value β(2).' Zudilin's determinantal criterion explained why known approximations fail for G
- Method (paper, §1.2): determinants of size 48N whose entries are moments of two kernels, 'Each moment is a rational linear combination of 1, G and ζ(2)'; high Taylor contact 'cancels the ζ(2) term in every entry', so G ∈ ℚ would make all determinants rational; denominator bounds then contradict an integral bound. Nonvanishing comes from a Frobenius reduction to three fixed rational matrices and 'An exact finite certificate'
- Earlier claim: Zhi-Wei Sun posted 'Catalan's constant is irrational' on arXiv on 3 Sep 2026 (2609.04176). The OpenAI paper (verbatim): 'Sun [22] has also announced a proof of the same qualitative irrationality statement. No result from that preprint is used here.'
- Lean: comparator challenge Catalan.lean states `theorem catalan_irrational : Irrational (∑' j : ℕ, (-1 : ℝ) ^ j / ((2 * j + 1 : ℕ) : ℝ) ^ 2)` using only Mathlib, standard axioms only; solution module OAI.NumberTheory.Catalan.Main. The series converges absolutely, so Mathlib's tsum is the usual sum G (our reading of the statement). The oai-math-revised comparator run (25–26 Oct) accepted it
- Frank Calegari (Persiflage, 8 Oct, verbatim): 'there are clearly a bunch of new ideas, or at least new optimizations, that we were not previously aware of'; 'certain optimizations are taking place without being motivated at all'; 'it’s amusing to see this paper cite two crank papers, both of which give nonsense proofs that Catalan’s constant is rational'. He is co-organising an irrationality conference at SLMath in January where these methods will be studied, and notes no analogous OpenAI proof for L(2, χ₋₃) yet
- Follow-ups: Sean Litsey (Hexagon 2610.00187, v5): 'Building on OpenAI’s proof that Catalan’s constant … is irrational, we prove |G − a/b| > b^−740', i.e. μ(G) ≤ 740, with a Lean formalization; its provenance says the work 'was produced entirely by Claude Opus 5.5 and GPT-6.1 Sol'. Community notes list further Zenodo and Hexagon preprints with weaker measures and extensions to other beta values (Jha, Carreira, Krisman)

## What happened

Catalan's constant, G ≈ 0.9159655, is the alternating sum of the reciprocals of the odd squares. Unlike ζ(2) = π²/6 and ζ(3)
(Apéry, 1978), it had resisted every attempt: known approximations to G converge fast, but their
denominators grow too fast for the classical irrationality criterion. The best results were statements that at least one value in a
short list of Dirichlet beta values is irrational.

OpenAI's manuscript proves G irrational directly. It assumes G = a/b, builds determinants of growing size from moments that mix 1, G
and ζ(2), arranges the construction so that the ζ(2) parts cancel, and shows that the determinants would have to be nonzero rational
numbers that are too small for their denominators. The nonvanishing step reduces, along a sequence of primes, to three fixed matrices
whose determinant is checked by an exact computation. The main theorem is formalized in Lean against a one-line statement that uses
only Mathlib's definitions.

## Why it matters

The irrationality of Catalan's constant is one of the best-known open questions about specific constants, listed with Euler's γ on
standard lists of unsolved problems. A Lean proof of a faithful one-line statement makes this one of the more trustworthy results in
the release, although no specialist has yet published a complete human reading of the argument.

## What is disputed or not yet verified

- Verification: Lean formalization of the main theorem (comparator accepted); no published human verification yet

## Reactions

### Reactions and follow-ups

Frank Calegari wrote that, as with the AI proof of the irrationality of ζ(5) in September, the paper contains new ideas or at least
new optimizations, often unmotivated, and noted that it cites two crank papers claiming G is rational. Zhi-Wei Sun had posted a
different proof claim on arXiv a month earlier; the OpenAI paper says it uses nothing from it. Outside authors, largely with AI
assistance, have since pushed the method to explicit irrationality measures (μ(G) ≤ 740 with a Lean development) and probed
extensions to β(4) and other values.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 189 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 128 days after its cutoff

## Sources

1. [OpenAI: Catalan's constant is irrational (24 Sep)](https://github.com/openai/math/blob/main/preprints/Catalans-constant-is-irrational-September-24-2026/paper.pdf) (github.com, paper)
2. [Lean scope note for family 005](https://github.com/openai/math/blob/main/lean/docs/005.md) (github.com, code)
3. [Lean comparator challenge: Catalan.lean](https://github.com/openai/math/blob/main/lean/ComparatorChallenges/Catalan.lean) (github.com, code)
4. [arXiv 2609.04176: Zhi-Wei Sun, Catalan's constant is irrational (3 Sep 2026)](https://arxiv.org/abs/2609.04176) (arxiv.org, paper)
5. [Hexagon 2610.00187: Sean Litsey, An Irrationality Measure for Catalan's Constant](https://hexagonmath.org/abs/2610.00187v5) (hexagonmath.org, paper)
6. [oai-math-revised: comparator run on all challenges (LEAN_CHECKS.md)](https://github.com/mathcommunity/oai-math-revised/blob/main/docs/LEAN_CHECKS.md) (github.com, code)
7. [Persiflage (Frank Calegari): A Brief Digest of Some New OpenAI Results (8 Oct)](https://galoisrepresentations.org/2026/10/08/a-brief-digest-of-some-new-openai-results/) (galoisrepresentations.org, discussion)
8. [oai-math-revised: community notes on the Catalan manuscript (follow-ups, Lean)](https://github.com/mathcommunity/oai-math-revised/blob/main/preprints/Catalans-constant-is-irrational-September-24-2026/AGENT_NOTES.md) (github.com, discussion)

## Changes

- 2026-10-29 (filed): Created (families 001–125; manuscript introduction, Lean statement, comparator results, Persiflage digest, Sun's arXiv abstract and the Litsey Hexagon page read)

## Related

- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-10-06: [OpenAI model claims the irrationality exponent of π is exactly 2 (Lean-formalized), which implies the Flint–Hills series converges](https://postcutoff.com/e/2026-10-06-irrationality-exponent-pi-openai/index.md)
- 2026-09-17: [ζ(5) proved irrational](https://postcutoff.com/e/2026-09-17-zeta-5-irrational-fauzan-lean-verified/index.md)