Irrationality of the dilogarithm at 1/2✓ Lean 4 verified · 3 standard axioms only
Ruiyi Zhang · Preprint, 2026-10-09 · 20 pages
PDFHTMLDOI 10.5281/zenodo.23251312Source and checks
Abstract
We prove that Li_2(1/2) is irrational. Irrationality of Li_2(1/s) was known for integers s ≤ −5 and s ≥ 6 by work of Hata and of Rhin and Viola, and Prellberg recently proved it for s = −4, 5, −3. The approximations come from determinants of moments of 1/(xy − 2), differentiated m/2 times in the parameter. We bound their values by a logarithmic energy on an ellipse, certified by directed interval arithmetic. Valuations of binomial coefficients give a common denominator of the coefficients. A Lucas congruence modulo 83 gives nonvanishing along m = 32 · 83^k. Three finite computations are part of the proof.
Formal verification
The main theorem is formalized in Lean 4 (Lean 4.35.0-rc4, Mathlib 25e572b8). The formal statement is
theorem li2_half_irrational :
Irrational (∑' k : ℕ, ((2 : ℝ)⁻¹) ^ (k + 1) / ((k : ℝ) + 1) ^ 2)
The theorem has no hypotheses. 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 1/2, preprint, Zenodo, 2026. https://doi.org/10.5281/zenodo.23251312