An Irrationality Measure for Catalan's Constant

Introduction

The result. Catalan’s constant

is the value at $s=2$ of the Dirichlet $L$-function of the nontrivial character modulo $4$. Values of $L$-functions at integers where no formula in terms of $\pi$ is available are notoriously hard to study. Apéry proved $\zeta(3)$ irrational in 1978 [1], and Calegari, Dimitrov and Tang proved $L(2,\chi_{-3})$ irrational in 2024 [5]. For $G$ the classical methods produce linear forms that do not decay fast enough, and its irrationality remained open. In October 2026 OpenAI [28] proved that $G$ is irrational, with a new argument based on a large determinant, and verified the proof in Lean. The present paper turns that argument into an irrationality measure.

The irrationality exponent $\mu(\xi)$ of a real number $\xi$ is the infimum of the real numbers $\mu$ such that $\lvert\xi-a/b\rvert>b^{-\mu}$ for all integers $a$ and all sufficiently large integers $b$. Every irrational number has $\mu(\xi)\ge2$, and almost every real number has $\mu(\xi)=2$. An irrationality measure is an explicit upper bound for $\mu(\xi)$. The exponent does not change under $\xi\mapsto r\xi+r'$ with $r,r'\in\mathbb{Q}$ and $r\ne0$.

The proof uses the prime number theorem. The theorem and every result it depends on have been verified in the Lean 4 proof assistant on top of OpenAI’s formalization. The formal proof has no unproved steps and uses only the standard axioms (§ 10). The use of AI in this work is disclosed at the end of the paper.

1.2. Background. Catalan’s constant. Irrationality proofs for values of $L$-functions at integers usually follow Apéry’s proof for $\zeta(3)$. One constructs linear forms $q_n\xi-p_n$ with integer coefficients that tend to zero faster than the coefficients grow. If $\lvert q_n\xi-p_n\rvert=e^{-\alpha n+o(n)}$ and $\lvert q_n\rvert=e^{\beta n+o(n)}$ with $\alpha>0$, then $\xi$ is irrational and $\mu(\xi)\le1+\beta/\alpha$. Beukers [3] obtained Apéry’s forms for $\zeta(2)$ and $\zeta(3)$ as integrals of Legendre-type polynomials. Hata [17] showed how much is gained by dividing the forms by the primes that divide all their coefficients, an idea that goes back to Chudnovsky. Rhin and Viola [31, 32] found finite groups acting on families of such integrals.

The invariance yields a large common factor of the coefficients, and this arithmetic method gave the best measures for $\zeta(2)$ and $\zeta(3)$ for many years. Marcovecchio [27] applied it to $\log2$, and Zeilberger and Zudilin [41] to $\pi$, using integrals of Salikhov [35]. For Catalan’s constant the analogous linear forms exist but do not decay fast enough. Rivoal and Zudilin [33] proved that one of the numbers $\beta(2), \beta(4), \ldots, \beta(2m)$ is irrational for suitable $m$, where $\beta$ is the Dirichlet beta function. This does not single out $G = \beta(2)$. Zudilin [43] found an Apéry-like recurrence for $G$, whose solutions give linear forms that tend to zero too slowly. Related constructions and their limits are described in [42, 20, 21, 46]. Eskandari, Murty and Nemoto [12] construct a mixed motive with period $G$ and obtain linear forms in 1 and $G$ from it, and Eskandari [11] improves their approximation exponent.

Recent results. Since September 2026 a series of new results in this area has appeared, several of them obtained with AI systems. OpenAI proved $\mu(\pi)=2$, with a Lean formalization [29]. Liu, Jiang and Zhang proved $\mu(\log r)=2$ for every rational $r>0$ with $r\ne1$ [26]. Giraudin lowered the bound for $\mu(\pi^2)$ to 5.0193784 with two hypergeometric constructions of Zudilin [44] at new parameters [15], and the bound for $\mu(\zeta(3))$ to 5.5138800 [16]. Leibtag, Barkan, Kalisch, Weinbaum, Shalyt and Kaminer [24] showed that the classical constructions are one-dimensional trajectories in conservative matrix fields. Searching over other trajectories, they obtained $\mu(\pi^2)<4.62675$ and $\mu(\zeta(3))<5.4197$, and further Apéry-like approximations to $G$, the best of which still has a negative approximation exponent. Prellberg [30] proved that $\operatorname{Li}_2(-1/4)$, $\operatorname{Li}_2(1/5)$ and $\operatorname{Li}_2(-1/3)$ are irrational. Fauzan announced a proof that $\zeta(5)$ is irrational, using Hankel determinants [13]. Lai combined this method with simultaneous approximations to show that 1, $\zeta(3)$ and $\zeta(4)$ are linearly independent over $\mathbb{Q}$ [22]. For $L(2,\chi_{-3})$ the effective holonomy bounds of Calegari, Dimitrov and Tang give $\mu(L(2,\chi_{-3}))\le24781$ [6 Thm. 5.1].

Determinant methods. OpenAI’s argument [28] has a different shape. Instead of a sequence of linear forms it uses one determinant $\Delta_N$ of size $n=48N$, whose entries are rational linear combinations of 1 and $G$. The entries are double integrals against the Cauchy kernel $1/(1-ts)$. If $G$ were rational, the denominators of the entries would force a lower bound

along $N=p$ prime. On the other hand, Andrieff’s identity [14] writes $\Delta_N$ as an integral of a product of determinants, and an estimate for a discrete logarithmic energy gives

OpenAI proves $D>\Lambda$, with a margin of about $10^{-4}$ per unit of $n^2$, and proves that $\Delta_p\ne0$ by reduction modulo $p$. Determinants of linear forms had been used for irrationality before, in Zudilin’s criterion with Hankel determinants [45].

The first irrationality measure for $G$ was obtained by Jha [18], who proved $\mu(G)\le10^8$. Carreira [8] treated the five integer parameters of the construction as free, stated conditions under which OpenAI’s argument goes through, and proved $\mu(G)<2294$. He also expressed the best constant of the energy estimate as the value of an equilibrium problem for two measures, and in [7] he records attempts to carry the method to $\beta(4)$. Bojnal [4] and Xu [40] obtained $\mu(G)<2402$ and $\mu(G)\le727.03$ at other parameters. Xu’s certificate is numerical and not formalized. Davis [9] and Arkhipov [2] reached $\mu(G)\le528.24$ with new quadrature nodes, the zeros of $T_K(P(t))$ for a fixed polynomial $P$, and Davis’s result is formalized in Lean. These constructions are independent of the ideas of the present paper. An earlier preprint of Sun [36] claimed the irrationality of $G$, but Wachs [39] showed that its main estimate is not justified.

The companion paper

Catalan’s constant is a difference of two values of the trigamma function $\psi'$. With

one has $G=\frac{1}{16}\Psi\left(\frac{1}{4},\frac{3}{4}\right)$. The companion paper [25] proves irrationality measures for $\Psi(s,1)$ with $s=\frac{k}{4},\frac{k}{3},\frac{k}{5},\frac{k}{7},\frac{k}{2}$, and for $\Psi\left(\frac{1}{3},\frac{2}{3}\right)=9L(2,\chi_{-3})$. For $\Psi\left(\frac{1}{4},1\right)$ and $\Psi\left(\frac{3}{4},1\right)$, which are rational multiples of $G\pm5\pi^2/48$, and for $s=\frac{k}{5},\frac{k}{7}$, these are the first proofs of irrationality that we know of. Its determinants are Löwner matrices of digamma differences, which are much smaller than OpenAI’s. That method also applies to $\left(\frac{1}{4},\frac{3}{4}\right)$, but there its denominators outgrow its decay, so it gives no measure for $G$. The present paper therefore refines OpenAI’s construction. The two papers use the same criterion, the same names for the denominator exponent $\Lambda$, the decay rate $D$ and the neighbourhood exponent $\rho$, and one formalization.

What a measure requires

Write $\Delta_N(X)=\det(A_N^0+XL_N)$, so that OpenAI’s determinant is $\Delta_N(G)$, and let $Q_N$ be the integer polynomial obtained by clearing denominators. Suppose $|G-a/b|$ is small. Three properties of $Q_N$ turn OpenAI’s comparison into a contradiction.

(i) Denominators. The coefficients of $\Delta_N$ have a common denominator of size $e^{(\Lambda+o(1))N^2}$, and $\deg Q_N\le dN$.

(ii) Smallness on a neighbourhood. $|\Delta_N(x)|\le e^{-(D+o(1))N^2}$ for every $x$ with $|x-G|\le e^{-\rho N}$, not only at $x=G$.

(iii) Nonvanishing at the point. $Q_p(a/b)\ne0$ for a prime $p$ of size about $\log b$.

OpenAI’s proof gives nonvanishing only at $X=G$. We need it at every $a/b$ with $p^2\nmid b$, and we must find such a prime without losing a power of $b$. § 2.4 shows that the squares of the larger primes can be recovered from the coefficients of $Q_p$.

Outline of the proof