HEXAGONbeta

Irrationality of χ2(1/q)\chi_2(1/q), Ti2(1/q)\mathrm{Ti}_2(1/q) and χ2(2/q)\chi_2(2/q)

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

Contributed by Shawn Krisman ↗

Version 1 / Nov 13, 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 and Ti2(z)=∑n≥0(−1)nz2n+1/(2n+1)2\mathrm{Ti}_2(z)=\sum_{n\ge0}(-1)^nz^{2n+1}/(2n+1)^2 the inverse tangent integral. We prove three theorems: χ2(1/q)\chi_2(1/q) is irrational for every integer q≥3q\ge3 with q≠4q\ne4; Ti2(1/q)\mathrm{Ti}_2(1/q) is irrational for every integer q≥5q\ge5; and χ2(2/q)\chi_2(2/q) is irrational for every odd integer q≥175q\ge175. All three come from one construction: the Hankel determinants of a moment functional with half-integer poles and geometric weight ww, read at w=q−2w=q^{-2}, w=−q−2w=-q^{-2} and w=4q−2w=4q^{-2}. Their denominators are bounded prime by prime, their size by a discrete log-gas argument against explicit dual certificates, and their nonvanishing by a reduction modulo an auxiliary prime. The three cases differ at the prime 22, where each needs its own lemma, in the certificates, and in how the nonvanishing lemma is transferred. For large qq the three statements follow from the linear independence criteria of David, Hirata-Kohno and Kawashima; for the first two, a 1990 criterion of Hata, which we could not consult, also applies from a threshold unknown to us. Below these ranges the results are new as far as we know. All three theorems are formalised in Lean 4 with Mathlib and checked by the Lean kernel, using only Lean's three standard axioms.

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. Bahç\ivan, Hasan Ekim. Irrationality of Re Lis\mathrm{Re}\,\mathrm{Li}_s, Tis\mathrm{Ti}_s, and related functions at almost all positive integers. 2026. November 8, 2026. Not peer reviewed. Zenodo, https://doi.org/10.5281/zenodo.24047688link
  3. 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
  4. David, Sinnou; Hirata-Kohno, Noriko; Kawashima, Makoto. Linear forms in polylogarithms. Ann. Sc. Norm. Super. Pisa Cl. Sci. (5), vol. 23, no. 3, pp. 1447–1490. 2022arXivDOI
  5. 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
  6. de Moura, Leonardo; Ullrich, Sebastian. The Lean 4 Theorem Prover and Programming Language. Automated Deduction – CADE 28, vol. 12699, pp. 625–635. 2021DOI
  7. 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
  8. Forrester, Peter J. Meet Andréief, Bordeaux 1886, and Andreev, Kharkov 1882–1883. Random Matrices Theory Appl., vol. 8, no. 2, pp. 1930001. 2019arXivDOI
  9. 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
  10. Hata, Masayoshi. Rational approximations to the dilogarithm. Trans. Amer. Math. Soc., vol. 336, no. 1, pp. 363–387. 1993. MR 1147401DOI
Show all 25 referencesShow fewer references
  1. 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
  2. Krisman, Shawn. χ2(1/3)\chi_2(1/3) and χ2(1/5)\chi_2(1/5) are irrational. 2026. Not peer reviewed; produced largely by AI models, see its disclosure. Hexagon 2610.00372v2, https://hexagonmath.org/abs/2610.00372v2; also file \textttpaper/chi2-irrationality.pdf in https://github.com/telaviv/chi2-irrationalityhexagon
  3. Krisman, Shawn. Lean formalisation: irrationality of χ2(1/q)\chi_2(1/q), Ti2(1/q)\mathrm{Ti}_2(1/q) and χ2(2/q)\chi_2(2/q). 2026. Commit 7a2780c73c5d84fc41e3ea49f56dabf7e13b0235. https://github.com/telaviv/chi2-irrationalitylink
  4. Lewin, Leonard. Polylogarithms and Associated Functions. North-Holland. 1981. Zbl 0465.33001
  5. 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
  6. 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
  7. 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
  8. 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
  9. Saff, Edward B.; Totik, Vilmos. Logarithmic Potentials with External Fields. Springer-Verlag, vol. 316. 1997DOI
  10. Tan, Hu; Zhang, Ying. Uniform cubic bounds for irrational values of the dilogarithm. 2026. Preprint; not peer reviewed (AI-assisted, see the paper's acknowledgments). arXiv:2611.01066
  11. 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
  12. 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
  13. The mathlib Community. mathlib4. 2026. Tag v4.35.0, commit 56a005855ea17e0b0958f73ec801ae140b0a1679. https://github.com/leanprover-community/mathlib4link
  14. Viola, Carlo; Zudilin, Wadim. Linear independence of dilogarithmic values. J. Reine Angew. Math., vol. 736, pp. 193–223. 2018DOI
  15. Zhang, Ruiyi. Irrationality of the dilogarithm at reciprocals of integers. 2026. October 19, 2026. With a Lean formalisation; not peer reviewed. Zenodo record 23296411 (version 2: https://doi.org/10.5281/zenodo.23482367)link

Version history

  1. v1 · 46 pagesSubmitted by Shawn KrismanInitial depositCurrentNov 13, 2026