{"id":"palomar/PALOMAR-2026-09-19-000004","url":"https://github.com/TaifengYi/zeta7-irrationality/tree/8af843a0536a8f1fc3945ef302d16fb2f6622b2a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-19-000004-v1.json","repo":"https://github.com/TaifengYi/zeta7-irrationality","tags":["math.NT","msc:11J72","msc:11S40","msc:11F33","msc:11F85","msc:11B68","msc:68V20","number-theory","p-adic-analysis","lean"],"score":0,"title":"Irrationality of the 7-adic zeta value ζ₇(3)","trust":"high","domain":"math.NT","source":"palomar","authors":["Yi Taifeng"],"reviews":0,"subject":"math.NT","summary":"A complete Lean 4 / Mathlib proof that the 7-adic zeta value ζ₇(3) is irrational. Here ζ₇(3) = L₇(3, ω⁻²) is the Kubota–Leopoldt value, equal to the 7-adic limit of the Euler-corrected Bernoulli numbers −(1 − 7^{w−1}) B_w / w over the weights w = 6·7^{n+1} − 2. The same is proved for η = ζ₇(3)/2. The proof is a determinant irrationality argument on the modular curve X₀(7), in four parts: independence of seven explicit germs attached to the weight −2 seven-adic Eisenstein series, with a uniform zero estimate; a seven-adic annular saving; an auxiliary-prime denominator estimate; and an…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-19","reactions":{},"formalized":true}