An Irrationality Measure for Catalan's Constant

Let $G=\sum_{j\ge0}(-1)^j(2j+1)^{-2}$ be Catalan's constant. We prove that $|G-a/b|>b^{-410}$ for all integers $a$ and all sufficiently large integers $b$. Hence the irrationality exponent of $G$ is at most $410$. The proof refines OpenAI's recent proof that $G$ is irrational. That proof compares two bounds for a large determinant whose entries are linear forms in $1$ and $G$. The lower bound comes from the denominators of the entries, and the upper bound from an integral representation. We improve both. On the arithmetic side we show that the matrix of rational parts has large corank modulo $p$ for every prime in an explicit range, which lowers the denominators. On the analytic side we bound a determinant that the energy method treats trivially, using Pick matrices, Heine's formula and an inequality for the logarithmic energy of signed measures. A quadrature formula extends the upper bound to an exponentially small neighbourhood of $G$, as a measure requires. The proof is formalized in the Lean proof assistant.