math.NT — Number Theory
A quasi-Riemann hypothesis for Dedekind zeta functions
Recent work on Artin's primitive root conjecture establishes a zero-free half-plane $\Rea s>1-10^{-6}$ for finite-order Hecke -functions over cyclotomic fields containing . Following their strategy, we prove that if is any number field, then the Dedekind zeta function does not vanish in the half-plane $\Rea s>1-1/6000$. As a corollary, the -function of any finite-order Hecke character defined over also does not vanish in the half-plane $\Rea s > 1-1/6000$. The proofs were generated and verified in Lean using AxiomProver. Compared to the work on Artin's primitive root conjecture, the hardest part was the formalization of the work of Kazhdan and Patterson on metaplectic forms in order to accommodate all number fields.