OpenAI: Catalan’s constant is irrational (Lean)

Your AI and this story

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)