{"id":"palomar/PALOMAR-2026-10-13-000010","url":"https://github.com/AxiomMath/DedekindZetaZeroFree/tree/09afbb4ce6570c1615d58509dc197fc9f0956b7d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-13-000010-v2.json","repo":"https://github.com/AxiomMath/DedekindZetaZeroFree","tags":["math.NT","msc:11M41","msc:11F70","analytic-number-theory","dedekind-zeta","lean"],"score":0,"title":"A uniform zero-free region for Dedekind zeta functions","trust":"high","domain":"math.NT","source":"palomar","authors":["Dean Cureton"],"reviews":0,"subject":"math.NT","summary":"A Lean formalization of Theorem 1.1 and Corollary 1.2 of A quasi-Riemann hypothesis for Dedekind zeta functions: for every number field K, its Dedekind zeta function has no zeros in Re(s) > 31/32. The formal statement asserts the existence of a holomorphic function away from 1 that agrees with Mathlib's Dedekind zeta function for Re(s) > 1 and is nonzero for Re(s) > 31/32 with s different from 1. The corollary gives the same zero-free bound for Hecke L-functions associated with finite-order Hecke characters, including s = 1 for nonprincipal characters. These characters are represented in…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-14","reactions":{},"formalized":true,"formalizes":[{"title":"A quasi-Riemann hypothesis for Dedekind zeta functions","identifier":"https://hexagonmath.org/2610.00200v1","relationship":"formalizes"}]}