math.NT — Number Theory

An Irrationality Measure for Catalan's Constant

Contributed by Sean Litsey

uilding on OpenAI's recent proof that Catalan's constant $G=\sum_{j\ge0}(-1)^j/(2j+1)^2$ is irrational, we prove that \[ \left|G-\frac ab\right|>b^{-8\,127} \] for all integers $a$ and all sufficiently large integers $b$. Thus the irrationality exponent of $G$ is at most $8\,127$; without the prime number theorem in the final step the same argument gives $23\,168$. The previous best bound, due to Jha, is $10^8$. The new ingredient is a perturbation estimate for OpenAI's determinant, viewed as a polynomial $\Delta_N(X)$ in the constant: on the interval $|x-G|\le e^{-404.25N}$ the polynomial moves by no more than OpenAI's bound for $|\Delta_N(G)|$. It is proved by a quadrature formula for the coefficient of the constant, an Andr\'eief identity with fixed columns, a generalized Vandermonde bound, and OpenAI's energy method rerun for configurations with fewer points. We also give a new certificate, with re-optimized trial sequences, for one of the two cases of OpenAI's logarithmic-energy dual; it raises the margin of the argument by a factor of almost eight. Every step, including the final theorem, is formalized in Lean~4 on top of OpenAI's formalization, without \texttt{sorry} and with only the standard axioms.