Irrationality of the dilogarithm at reciprocals of integers✓ Lean 4 verified · 3 standard axioms only
Ruiyi Zhang · Preprint, 2026-10-11 · 57 pages
PDFHTMLDOI 10.5281/zenodo.23296411Source and checks
Abstract
We prove that Li_2(1/n) is irrational for every nonzero integer n. The proof combines a determinant criterion with exact fixed-base integerization, logarithmic-potential estimates, Frobenius nonvanishing, and a three-form Hermite–Padé construction. The finite positive range is treated by a common variational problem and two endpoint certificates; the negative middle range is handled by signed contour integrals at the six bases −2, …, −7; the two remaining tails follow from an explicit Hermite–Padé estimate. Every numerical constant used in the argument is given as a rational bound or an explicitly directed interval.
Formal verification
The main theorem is formalized in Lean 4 (Lean 4.35.0-rc4, Mathlib 25e572b8). The formal statement is
theorem li2_inv_irrational (n : ℤ) (hn : n ≠ 0) :
Irrational (∑' k : ℕ, ((n : ℝ)⁻¹) ^ (k + 1) / ((k : ℝ) + 1) ^ 2)
The only hypothesis is n ≠ 0. The proof uses only the axioms propext, Classical.choice and Quot.sound, and is accepted by the Lean kernel and by the independent nanoda kernel. Files: lean/. An interactive map of the formal proof and its dependencies: Lean proof map.
Cite
Ruiyi Zhang, Irrationality of the dilogarithm at reciprocals of integers, preprint, Zenodo, 2026. https://doi.org/10.5281/zenodo.23296411