math.NT — Number Theory
χ₂(1/3) and χ₂(1/5) are irrational
Let be Legendre's chi function. We prove that and are irrational. Equivalently, for . The proof uses the Hankel determinants of the moment functional , where . These determinants are values of polynomials of degree at most . We bound the denominators of 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 , and . We bound the size of by a discrete log-gas argument against an explicit dual certificate, and prove that for every rational and infinitely many , through a reduction modulo an auxiliary prime . The margins are below () and () per . 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.