{"id":"palomar/PALOMAR-2026-09-25-000023","url":"https://github.com/gmDevi/zeta2-7-9-11-lean/tree/2ae1bccb82f1f72ed7a7aeab3196aa1cdbee165a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000023-v1.json","repo":"https://github.com/gmDevi/zeta2-7-9-11-lean","tags":["math.NT","msc:11J72","msc:11S40","msc:11S80","msc:11M06","msc:33C20","p-adic-zeta","lean-formalization","number-theory","irrationality"],"score":0,"title":"At least one of the 2-adic zeta values ζ₂(7), ζ₂(9), ζ₂(11) is irrational","trust":"high","domain":"math.NT","source":"palomar","authors":["Gennaro Marco Devincenzis"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 and Mathlib proof that at least one of the 2-adic zeta values ζ₂(7), ζ₂(9), ζ₂(11) is irrational. The theorem has no hypotheses, and its proof uses only the axioms propext, Classical.choice and Quot.sound. The values are defined through the Volkenborn integral: zeta2 s = J(s−1)/((s−1)·2^s), where J(s) is the 2-adic limit of the Riemann sums 2^(−N) Σ_{x<2^N} (x+1/2)^(−s), and the theorem also proves that these limits exist. By Lemma 2.8 of Lai, Sprang and Zudilin (IMRN 2026), zeta2 s is the Kubota–Leopoldt value ζ₂(s) = L₂(s, ω^(1−s)) for s ≥ 2. That identification is cited, not…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-25","reactions":{},"formalized":true}