{"id":"palomar/PALOMAR-2026-09-30-000007","url":"https://github.com/gmDevi/zeta-7-21-lean/tree/a3b69fc43aea3dd140540f6e8380c7d0fecce028","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000007-v1.json","repo":"https://github.com/gmDevi/zeta-7-21-lean","tags":["math.NT","msc:11J72","msc:11M06","msc:33C20","lean","number-theory","zeta-values","irrationality"],"score":0,"title":"At least one of ζ(7), ζ(9), …, ζ(21) 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 eight values ζ(7), ζ(9), ζ(11), ζ(13), ζ(15), ζ(17), ζ(19), ζ(21) of the Riemann zeta function is irrational. The statement uses only Mathlib's riemannZeta, the theorem has no hypotheses, and its proof uses only the axioms propext, Classical.choice and Quot.sound. The shortest list of odd zeta values starting at ζ(7) that our literature search found proved to contain an irrational number was ζ(7), ζ(9), …, ζ(35) (W. Zudilin, Math. Notes 2001). The proof uses the very-well-poised linear forms of Zudilin (J. Théor. Nombres Bordeaux 2004, §8)…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true}