Irrationality of Catalan’s Constant

Irrationality of Catalan’s Constant

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 005; 2026-09-24), the asserted result is that Catalan's constant is irrational.

Mathematical statement of the claimed result

Manuscript 1.

The claimed irrationality assertion is \[ G=\sum_{n=0}^{\infty}\frac{(-1)^n}{(2n+1)^2}\notin\mathbb Q. \] This is Catalan's constant, defined by its absolutely convergent series.

Outline of the argument

For manuscript 1 (family 005; 2026-09-24), polynomial moment rows are arranged so that contact conditions eliminate the unwanted zeta value. A nonzero determinant is bounded at the real place and at finite primes, with a separate two-adic calculation; denominator clearing makes these bounds contradictory under rationality.

Formal verification

For manuscript 1 (family 005; 2026-09-24), OpenAI lists Lean statements for this assertion: Catalan's constant is irrational.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

The linked family Comparator checks are Catalan.lean.

Their named declarations include OAI.InternalCatalan.catalan_irrational.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

• OpenAI, Catalan's constant is irrational, 2026-09-24; citation key OAI:Catalans-constant-is-irrational-September-24-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main.
• Family 005: Lean scope.
• Comparator Catalan.json.
• Comparator Catalan.lean.
• OpenAI catalogue entry.

Irrationality of Catalan’s Constant

Definitions and mathematical statement

Catalan's constant is the convergent alternating series \[ G=\beta(2)=\sum_{n=0}^{\infty}\frac{(-1)^n}{(2n+1)^2}, \] where $\beta(s)=\sum_{n\ge0}(-1)^n(2n+1)^{-s}$ is the Dirichlet beta function in its region of convergence. Determine whether $G\notin{\mathbb{Q}}$, equivalently whether $bG-a\ne0$ for every $a\in{\mathbb{Z}}$, $b\ge1$. This is the value at two, not a general assertion about all beta values or an odd beta value with a different explicit formula. Proving transcendence is not necessary, and arbitrarily accurate decimal computation alone cannot exclude an unrestricted rational denominator.

Formulation and concept references: [S1].

Short English statement

Is Catalan's constant, the alternating sum of reciprocal odd squares, irrational?

Research attempt

Process and selected irrationality route.

This attempt was generated by GPT-6 Astra Ultra on 27 September 2026. We construct rational approximations from the defining alternating series and from an accelerated integral expansion. We prove exact positive remainder formulas and analyze the denominators that a standard integer-linear-form argument would have to clear. Both natural clearing procedures fail to produce forms tending to zero. A finite rational-exclusion calculation is also made, with its denominator bound stated explicitly.

The formulation source [S1] studies integral approaches to irrationality and the distinction between promising candidates and completed proofs. No irrationality theorem for this particular constant is imported from that work. We aim at the catalogue's exact assertion: every rational candidate must be excluded, not merely the candidates with denominators below a large computational cutoff.

A positive integral representation.

For $0\le x\le1$, finite geometric summation gives \[ \frac1{1+x^2}=\sum_{n=0}^{N-1}(-1)^nx^{2n} +\frac{(-1)^Nx^{2N}}{1+x^2}. \] Multiplying by $-\log x$ and integrating, with \[ \int_0^1x^{2n}(-\log x)\,dx=\frac1{(2n+1)^2}, \] shows that \[ G=\int_0^1\frac{-\log x}{1+x^2}\,dx, \qquad 0<G<1. \tag{413.1} \] Indeed the absolute value of the integrated remainder is at most $(2N+1)^{-2}$, which tends to zero. This argument uses finite sums plus an explicit remainder, so no unproved interchange of a conditionally convergent series and an integral is needed.

Let $S_N=\sum_{n=0}^{N-1}(-1)^n/(2n+1)^2$. The same identity gives the exact signed remainder \[ R_N=(-1)^N(G-S_N) =\int_0^1\frac{x^{2N}(-\log x)}{1+x^2}\,dx>0. \] Since $1/2\le(1+x^2)^{-1}\le1$, \[ \frac1{2(2N+1)^2}\le R_N\le\frac1{(2N+1)^2}. \tag{413.2} \] The positivity supplies nonvanishing; the issue is whether smallness survives clearing denominators.

The integer-linear-form criterion.

If integers $A_N,B_N$ satisfy \[ 0<|A_NG-B_N|\longrightarrow0, \tag{413.3} \] then $G$ is irrational. To prove this, suppose $G=a/b$ with integers $a,b$ and $b>0$. Multiplication by $b$ makes every form a nonzero integer, hence of absolute value at least one, contradicting convergence to zero.

Small rational approximation errors alone do not imply $413.3$. The multiplier required to turn the rational approximant into an integer must be included in the estimate. This is the point tested in both constructions below.

The direct partial sums lose too much to denominators.

Let \[ L_N=\operatorname{lcm}(1,3,5,\ldots,2N-1). \] Then $L_N^2S_N\in\mathbb Z$, so a natural candidate form is $L_N^2G-L_N^2S_N$. We establish an elementary exponential lower bound for $L_N$, without invoking a prime number theorem.

The central binomial coefficient $\binom{2N}{N}$ divides $\operatorname{lcm}(1,2,\ldots,2N)$. For each prime $p$, its valuation is \[ \sum_{j\ge1}\left(\left\lfloor\frac{2N}{p^j}\right\rfloor -2\left\lfloor\frac{N}{p^j}\right\rfloor\right). \] Each nonzero summand is $1$, and there are at most $\lfloor\log_p(2N)\rfloor$ summands, the exponent of $p$ in that least common multiple. This proves the divisibility prime by prime. Removing its power of $2$ leaves exactly $L_N$, and that removed power is at most $2N$. Also $\binom{2N}{N}\ge4^N/(2N+1)$ because it is the largest of the $2N+1$ binomial coefficients whose sum is $4^N$. Hence \[ L_N\ge\frac{4^N}{2N(2N+1)}. \tag{413.4} \] Combining $413.2$ and $413.4$ yields \[ |L_N^2G-L_N^2S_N| \ge\frac{16^N}{8N^2(2N+1)^4}\longrightarrow\infty. \tag{413.5} \] Thus this particular denominator-cleared family fails the required smallness as strongly as possible. This is not a theorem that every rational approximation obtained from the series must fail. The chosen multiplier is a universal clearing factor and need not be the reduced denominator; substantial arithmetic cancellations would require a separate analysis.

Acceleration from an exact geometric identity.

Write \[ \frac1{1+x^2}=\frac12\sum_{k=0}^{\infty} \left(\frac{1-x^2}{2}\right)^k. \] All summands are nonnegative on $[0,1]$. Integrating gives \[ G=\sum_{k=0}^{\infty}\frac{a_k}{2^{k+1}},\qquad a_k=\int_0^1(1-x^2)^k(-\log x)\,dx =\sum_{j=0}^k\frac{(-1)^j\binom kj}{(2j+1)^2}>0. \tag{413.6} \] Let $Q_N$ be the sum of the first $N$ terms. Its positive error has the exact integral form \[ E_N=G-Q_N =\int_0^1\frac{-\log x}{1+x^2} \left(\frac{1-x^2}{2}\right)^Ndx. \tag{413.7} \] In particular $0<E_N\le2^{-N}G<2^{-N}$, an exponential improvement over the direct remainder. The accelerated sums provide efficient rational intervals containing $G$.

However, all denominators in $Q_N$ are cleared by $D_N=2^NL_N^2$. On $0<x\le N^{-1/2}$, for $N\ge2$, we have \[ (1-x^2)^N\ge(1-1/N)^N\ge1/4,\qquad -\log x\ge\tfrac12\log N,\qquad (1+x^2)^{-1}\ge1/2. \] Restricting the integral $413.7$ to this interval gives \[ E_N\ge\frac{2^{-N}\log N}{16\sqrt N},\qquad D_NE_N\ge\frac{L_N^2\log N}{16\sqrt N}\longrightarrow\infty. \tag{413.8} \] Again $D_NQ_N$ is an integer, but the resulting nonzero integer-linear-form candidate does not tend to zero. Exponential analytic convergence is therefore insufficient for this clearing factor. The denominator contribution must be compared with the remainder on the same scale.

A finite exclusion result that really follows.

The strict interval \[ Q_N<G<Q_N+2^{-N} \tag{413.9} \] has rational endpoints. For any fixed denominator bound $B$, exact arithmetic can test whether it contains a fraction $a/b$ with $1\le b\le B$: multiply both endpoints by each $b$ and check for an integer strictly between them. Because $G\in(0,1)$, only finitely many numerators could qualify for each denominator. The accompanying check uses $N=40$ and excludes all such fractions with $b\le1000$.

This is a proved finite-denominator statement once the exact rational interval check is performed. It is not an irrationality proof. A rational number with denominator greater than $1000$ is not excluded by that calculation, and the fact that the test can be rerun at larger bounds does not show that every run succeeds. For a hypothetical rational $G=a/b$, sufficiently narrow intervals would always retain that particular fraction. Proving success for every $B$ would itself require an additional theorem.

An integer relation search has the same limitation when used without certified error bounds. A failure to find a small relation can suggest a direction but cannot establish the universal nonvanishing statement. Here the exact endpoints make the finite conclusion reliable, while leaving its quantifier visibly finite.

What would need to change in an integral approach.

The positive integrals have solved the nonvanishing side of $413.3$. The obstruction is arithmetic size. One possible route would be a different family of rational functions whose integrals have the form $A_NG-B_N$ with integer coefficients after a smaller normalization, while the integral decays faster than that normalization grows. Alternatively, a precise divisibility theorem could reduce the effective denominators of a constructed family. No such theorem is proved here. Merely optimizing the numerical convergence of $Q_N$ leaves the calculation $413.8$ untouched.

Verification and outcome.

The checks use rational arithmetic to verify the finite coefficient formula in $413.6$, denominator divisibility, the central-binomial least-common-multiple property for a finite range, and the exclusion in $413.9$. Positivity and the asymptotic failures of the two clearing procedures are established by the integral inequalities above, not by floating-point values of $G$.

UNRESOLVED. We obtain rigorous rational enclosures and finite-denominator exclusions, together with precise failures of two natural irrationality arguments. No sequence satisfying $413.3$, and no rational value for $G$, is established.

Sources

• S1 Tweaking the Beukers Integrals In Search of More Miraculous Irrationality Proofs A La Apery (Dougherty-Bliss, Koutschan, Zeilberger). https://arxiv.org/abs/2101.08308. Formulation source.