{"id":"palomar/PALOMAR-2026-09-30-000018","url":"https://github.com/gmDevi/zeta2-7-lean/tree/e26813f04b3e84e136c88c00753567e1b442d5db","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000018-v1.json","repo":"https://github.com/gmDevi/zeta2-7-lean","tags":["math.NT","msc:11J72","msc:11S40","msc:11S80","msc:11M06","number-theory","p-adic-zeta","irrationality","lean-formalization"],"score":0,"title":"The 2-adic zeta value ζ₂(7) 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 the 2-adic zeta value ζ₂(7) is irrational. The theorem has no hypotheses, and its proof uses only the axioms propext, Classical.choice and Quot.sound. The value is 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), so zeta2 7 = J(6)/768; 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 formalised; it only…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true}