HEXAGONbeta

Irrationality of χ₂ and Ti₂ at units of real quadratic fields

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

Contributed by Shawn Krisman ↗

Version 1 / Nov 11, 2026 / CC BY 4.0

Abstract

We prove that χ2(m2+1−m)\chi_2(\sqrt{m^2+1}-m), a value of Legendre's chi function at a unit of norm −1-1, is irrational for every integer m≥2m\ge2 except m=3,5,7,9,15m=3,5,7,9,15. For m=2m=2 this shows that π2−18log⁡2φ\pi^2-18\log^2\varphi is irrational, where φ\varphi is the golden ratio. The method extends to all units of norm −1-1 in real quadratic fields, giving χ2(ε)∉Q\chi_2(\varepsilon)\notin\mathbb{Q} outside an explicit set of 4747 units, and, through a twist identity, to the inverse tangent integral Ti2\mathrm{Ti}_2 at units of norm +1+1, outside 5757 units. The proof combines Hankel determinants of a reflection-symmetric Padé machine, arithmetic bounds on their denominators, a discrete log-gas bound certified in interval arithmetic, and a nonvanishing argument modulo a prime. Below the range covered by the criteria of David, Hirata-Kohno and Kawashima, these results appear to be new. All three theorems are formalised in Lean 4 with Mathlib, using only the standard axioms.

Tools used

Anthropic
Claude OpusVersion 5.5

References

  1. Baker, Alan. Transcendental Number Theory. Cambridge University Press. 1975DOI
  2. Calegari, Frank; Dimitrov, Vesselin; Tang, Yunqing. The linear independence of 11, ζ(2)\zeta(2), and L(2,χ−3){L}(2,\chi_{-3}). 2024. Preprint. arXiv:2408.15403arXiv
  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. Hakimoglu-Brown, Cetin. Collapsing fifty dilogarithm arguments to five terms over Q(u,4−3u2)\mathbb{Q}(u,\sqrt{4-3u^2}). 2026. Preprint, v1, August 24, 2026; not peer reviewed. arXiv:2608.23792arXiv
  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 32 referencesShow fewer references
  1. Hata, Masayoshi. The irrationality of log⁡(1+1/q)log⁡(1−1/q)\log(1+1/q)\log(1-1/q). Trans. Amer. Math. Soc., vol. 350, no. 6, pp. 2311–2327. 1998DOI
  2. Johansson, Fredrik. Arb: efficient arbitrary-precision midpoint-radius interval arithmetic. IEEE Trans. Comput., vol. 66, no. 8, pp. 1281–1292. 2017DOI
  3. Kawashima, Makoto. Linear independence of periods related to polylogarithms. 2026. Preprint, May 2026; not peer reviewed. arXiv:2605.17756arXiv
  4. 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
  5. Krisman, S. χ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
  6. Krisman, S. Irrationality of χ2\chi_2 and Ti2\mathrm{Ti}_2 at units of real quadratic fields: a Lean 4 proof. 2026. Lean proof, this paper, and the computation scripts (folder \textttscripts/paper). https://github.com/telaviv/chi2-quadratic-units-irrationalitylink
  7. Krisman, S. Lean formalisation: χ2(1/3)\chi_2(1/3) and χ2(1/5)\chi_2(1/5) are irrational. 2026. Commit 35b030db9fdae70b97583f6ded0781bf1b379fdc. https://github.com/telaviv/chi2-irrationalitylink
  8. Lewin, Leonard. Polylogarithms and Associated Functions. North-Holland. 1981. Zbl 0465.33001
  9. Lewin, Leonard. The dilogarithm in algebraic fields. J. Austral. Math. Soc. Ser. A, vol. 33, no. 3, pp. 302–330. 1982DOI
  10. 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
  11. Niven, Ivan. Irrational Numbers. Mathematical Association of America, no. 11. 1956
  12. Orr, Martin. Explicit height bounds for G-functions and unlikely intersections with lines in tori. 2026. Preprint, July 2026; not peer reviewed. arXiv:2607.09565arXiv
  13. 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). arXiv:2609.06895arXivDOI
  14. 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
  15. Rhin, Georges; Viola, Carlo. Linear independence of 11, Li1{\rm Li}_1 and Li2{\rm Li}_2. Mosc. J. Comb. Number Theory, vol. 8, no. 1, pp. 81–96. 2019DOI
  16. Saff, Edward B.; Totik, Vilmos. Logarithmic Potentials with External Fields. Springer-Verlag, vol. 316. 1997DOI
  17. 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.01066arXiv
  18. 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
  19. The FLINT team. python-flint: Python bindings for FLINT. 2026. Version 0.9.0. https://github.com/flintlib/python-flintlink
  20. 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
  21. The mathlib Community. mathlib4. 2026. Tag v4.35.0, commit 56a005855ea17e0b0958f73ec801ae140b0a1679. https://github.com/leanprover-community/mathlib4link
  22. Viola, Carlo; Zudilin, Wadim. Linear independence of dilogarithmic values. J. Reine Angew. Math., vol. 736, pp. 193–223. 2018DOI

Version history

  1. v1 · 59 pagesSubmitted by Shawn KrismanInitial depositCurrentNov 10, 2026