HEXAGONbeta

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

Primarily AI-generated textHuman understanding: no partsmath.NT — Number Theory

Contributed by Shawn Krisman ↗

Version 1 / Oct 20, 2026 / CC BY 4.0

Abstract

Let χ2(z)=∑n≥0z2n+1/(2n+1)2\chi_2(z)=\sum_{n\ge0}z^{2n+1}/(2n+1)^2 be Legendre's chi function. We prove that χ2(1/3)\chi_2(1/3) and χ2(1/5)\chi_2(1/5) are irrational. Equivalently, Li2(1/q)−Li2(−1/q)∉Q\mathrm{Li}_2(1/q)-\mathrm{Li}_2(-1/q)\notin\mathbb{Q} for q=3,5q=3,5. The proof uses the Hankel determinants Δh(χ2(1/q))\Delta_h(\chi_2(1/q)) of the moment functional g↦∑t≥1q−2t(g(u) u/Dh(u))′∣u=tg\mapsto\sum_{t\ge1}q^{-2t}(g(u)\,u/D_h(u))'|_{u=t}, where Dh(u)=∏k<h(u+k+1/2)D_h(u)=\prod_{k<h}(u+k+1/2). These determinants are values of polynomials Δh(X)∈Q[X]\Delta_h(X)\in\mathbb{Q}[X] of degree at most hh. We bound the denominators of Δh(X)\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 22, 33 and qq. We bound the size of Δh(χ2(1/q))\Delta_h(\chi_2(1/q)) by a discrete log-gas argument against an explicit dual certificate, and prove that Δh(a/b)≠0\Delta_h(a/b)\neq0 for every rational a/ba/b and infinitely many hh, through a reduction modulo an auxiliary prime ℓ=h/3\ell=h/3. The margins are below −0.054-0.054 (q=3q=3) and −0.256-0.256 (q=5q=5) per h2h^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.

Provenance statement

Claude Code was used to research and write the proof + formalization.

Tools used

Anthropic
Claude OpusVersion 5.5

References

  1. Andréief, C. Note sur une relation entre les intégrales définies des produits des fonctions. Mém. Soc. Sci. Phys. Nat. Bordeaux (3), vol. 2, pp. 1–14. 1886. Signed Kharkov, December 1883; often cited with the year 1883 (see Forrester, Random Matrices Theory Appl. 8 (2019) 1930001)
  2. David, Sinnou; Hirata-Kohno, Noriko; Kawashima, Makoto. Can polylogarithms at algebraic points be linearly independent?. Mosc. J. Comb. Number Theory, vol. 9, no. 4, pp. 389–406. 2020arXivDOI
  3. David, Sinnou; Hirata-Kohno, Noriko; Kawashima, Makoto. Linear independence criteria for generalized polylogarithms with distinct shifts. Acta Arith., vol. 206, no. 2, pp. 127–169. 2022arXivDOI
  4. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021DOI
  5. Del Solar, César. ζ(5)\zeta(5) is irrational: a Lean 4 formalization. 2026. Source of the port of the prime number theorem used here (commit 3da8eb1b91f9a90a1c0b7959e845c060dbd16256, 23 September 2026). https://github.com/domino14/zeta5link
  6. Forrester, Peter J. Meet Andréief, Bordeaux 1886, and Andreev, Kharkov 1882–1883. Random Matrices Theory Appl., vol. 8, no. 2, pp. 1930001. 2019arXivDOI
  7. Hata, Masayoshi. On the linear independence of the values of polylogarithmic functions. J. Math. Pures Appl. (9), vol. 69, no. 2, pp. 133–173. 1990. Zbl 0712.11040
  8. Hata, Masayoshi. Rational approximations to the dilogarithm. Trans. Amer. Math. Soc., vol. 336, no. 1, pp. 363–387. 1993. MR 1147401DOI
  9. Kontorovich, Alex; Tao, Terence; others. PrimeNumberTheoremAnd. 2026. Lean project, Apache License 2.0; the formalisation uses files from commit a5154676af9aa3095150ee410cdda80555aa0642 (30 August 2026). https://github.com/AlexKontorovich/PrimeNumberTheoremAndlink
  10. Krisman, Shawn. Lean formalisation: χ2(1/3)\chi_2(1/3) and χ2(1/5)\chi_2(1/5) are irrational. 2026. Commit 0d781d258e496d32c8997746654b6b42cb35fd89. https://github.com/telaviv/chi2-irrationalitylink
Show all 21 referencesShow fewer references
  1. Krisman, Shawn. Lean formalisation: one of β(4),β(6),…,β(36)\beta(4),\beta(6),\dots,\beta(36) is irrational. 2026. Release v1.0, commit f8df497467901e09fa497553f00d8ffa4480a46d. https://github.com/telaviv/beta-irrationalitylink
  2. Lewin, Leonard. Polylogarithms and Associated Functions. North-Holland. 1981. Zbl 0465.33001
  3. Liu, Si-Qi. Li2Rational: Lean 4 proofs of the irrationality of Li2(r)\mathrm{Li}_2(r) at certain rational points rr. 2026. Accessed 2026-10-18 (commit b2a61c4). Lean formalisation, not peer reviewed; AI-assisted per README. GitHub repository, https://github.com/siqiliu-tsinghua/Li2Rationallink
  4. Pólya, George. Remarks on characteristic functions. Proceedings of the [First] Berkeley Symposium on Mathematical Statistics and Probability (August 1945 and January 1946), pp. 115–123. 1949. Zbl 0038.28707
  5. Prellberg, Thomas. Three irrationality results for the dilogarithm: Rhin–Viola and Viola–Zudilin constructions at −1/4-1/4, 1/51/5, and −1/3-1/3. 2026. Preprint, September 7, 2026; not peer reviewed (AI-assisted, see the paper's statement on AI assistance)arXivDOI
  6. Rhin, Georges; Viola, Carlo. The permutation group method for the dilogarithm. Ann. Sc. Norm. Super. Pisa Cl. Sci. (5), vol. 4, no. 3, pp. 389–437. 2005. MR 2185863, Zbl 1170.11316
  7. Saff, Edward B.; Totik, Vilmos. Logarithmic Potentials with External Fields. Springer-Verlag, vol. 316. 1997DOI
  8. Tang, Qian. Irrationality of Li2(1/2)\mathrm{Li}_2(1/2): a Lean 4 proof. 2026. Accessed 2026-10-18 (commit 950ee9d). Lean formalisation, no accompanying paper found, not peer reviewed. GitHub repository, https://github.com/dtq1997/li2-half-irrationalitylink
  9. The mathlib Community. The Lean mathematical library. Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp. 367–381. 2020. arXiv:1910.09336arXivDOI
  10. The mathlib Community. mathlib4. 2026. Tag v4.35.0, commit 56a005855ea17e0b0958f73ec801ae140b0a1679. https://github.com/leanprover-community/mathlib4link
  11. Viola, Carlo; Zudilin, Wadim. Linear independence of dilogarithmic values. J. Reine Angew. Math., vol. 736, pp. 193–223. 2018DOI

Version history

  1. v1Submitted by Shawn KrismanInitial depositCurrentOct 18, 2026