math.NT — Number Theory

χ₂(1/3) and χ₂(1/5) are irrational

Contributed by Shawn Krisman

Let $\chi_2(z)=\sum_{n\ge0}z^{2n+1}/(2n+1)^2$ be Legendre's chi function. We prove that $\chi_2(1/3)$ and $\chi_2(1/5)$ are irrational. Equivalently, $\mathrm{Li}_2(1/q)-\mathrm{Li}_2(-1/q)\notin\mathbb{Q}$ for $q=3,5$. The proof uses the Hankel determinants $\Delta_h(\chi_2(1/q))$ of the moment functional $g\mapsto\sum_{t\ge1}q^{-2t}(g(u)\,u/D_h(u))'|_{u=t}$, where $D_h(u)=\prod_{k<h}(u+k+1/2)$. These determinants are values of polynomials $\Delta_h(X)\in\mathbb{Q}[X]$ of degree at most $h$. We bound the denominators of $\Delta_h(X)$ prime by prime: a bound adapted to residue classes for the large primes, a Lagrange-basis bound for the small ones, and separate arguments for the primes $2$, $3$ and $q$. We bound the size of $\Delta_h(\chi_2(1/q))$ by a discrete log-gas argument against an explicit dual certificate, and prove that $\Delta_h(a/b)\neq0$ for every rational $a/b$ and infinitely many $h$, through a reduction modulo an auxiliary prime $\ell=h/3$. The margins are below $-0.054$ ($q=3$) and $-0.256$ ($q=5$) per $h^2$. The whole proof, including the prime number theorem and both numerical certificates, has been formalised in Lean 4 with Mathlib and checked by the Lean kernel, using only Lean's three standard axioms.