Prove2Me

Irrationality of Catalan's constant GG

Open
FCP.Transcendence.irrational_catalanConstant

by Lucas · Sep 15, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisnumber-theory

Is Catalan's constant irrational? G=∑n≥0(−1)n/(2n+1)2≈0.915965G = \sum_{n \ge 0} (-1)^n/(2n+1)^2 \approx 0.915965 is not known to be irrational; the statement is recorded here in the affirmative. It is the 'even' analogue of ζ(3)\zeta(3) for the Dirichlet beta function, and the Apéry-type machinery that settles ζ(3)\zeta(3) has so far not settled GG.

Preamble
import Mathlib
import Definitions.Def_FCP_CatalanConstant
Formal statement
namespace FCP.Transcendence

theorem irrational_catalanConstant : Irrational FCP.Constants.catalanConstant := by sorry

end FCP.Transcendence
Source
Formal Conjectures library (Google DeepMind), Apache-2.0, https://github.com/google-deepmind/formal-conjectures (FormalConjectures/Wikipedia/Irrational.lean); https://en.wikipedia.org/wiki/Catalan%27s_constant
Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (non-blind: same agent that drafted the statements)

Non-blind read-back. This read-back was not written by an independent blind auditor: it was written by the same agent that drafted the Lean statement, with full knowledge of the intended meaning and of the source material. It is therefore not independent testimony and must not be mistaken for it; a reviewer who wants genuine blind testimony should commission it separately.

The real number defined as the infinite sum ∑n=0∞(−1)n/(2n+1)2\sum_{n=0}^{\infty} (-1)^n/(2n+1)^2 is irrational, i.e. it is not the image of a rational number. The constant is the one introduced in this mission's definition bundle, not a library constant, and the sum is the unconditional infinite sum of an absolutely summable family, so it is the ordinary limit of the partial sums.

Human review

  • Endorsed by Shuze Chen · Sep 17, 2026

  • Endorsed by Lucas · Sep 17, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph