Papers With

← All papers
First page of An asymptotic Jensen-Polya criterion for GRH

An asymptotic Jensen-Polya criterion for GRH

Ken Ono

math.NT Oct 28, 2026 · v1
formalization autoformalization mathlib number-theory
Read PDF arXiv abstract Code
TL;DR
Main theorem on zeros of unshifted Jensen polynomials for Dedekind zeta-functions is autoformalized in Lean 4 with Mathlib by AxiomProver, with public repository.
Abstract
The Jensen–Pólya criterion expresses the generalized Riemann hypothesis (GRH) for Dedekind zeta-functions as a real-rootedness condition on their Jensen polynomials. Previous asymptotic results require large shifts, while computations establish real-rootedness in the Riemann case through a finite range of degrees. Here we study the unshifted family as the degree tends to infinity. For every number field $K$, we prove unconditionally that $J_{K,d}(X)$ is nonzero and has at least $d-C_K\sqrt{d\log d}$ distinct negative real zeros for all sufficiently large $d$, where $C_K>0$ depends only on $K$. Therefore, the proportion of real zeros tends to one with error $O_K(\sqrt{\log d/d})$. The main theorems have been autoformalized in Lean 4 by AxiomProver.
Problem

The Jensen–Pólya criterion makes GRH for Dedekind zeta-functions equivalent to all unshifted Jensen polynomials J_{K,d} being real-rooted. Earlier asymptotic results needed large shifts, and computations cover only finitely many degrees.

Approach

The rescaled reciprocal Jensen polynomial is written as a Cauchy integral of the completed Dedekind zeta-function. Stirling's formula and Euler-product bounds feed a saddle-point analysis on circles through two conjugate saddles, using a uniform complex Gaussian estimate. This gives an oscillatory cosine formula whose sign changes are counted from the net phase change. AxiomProver carried out detailed calculations and produced a Lean 4 / Mathlib formalization of the main theorem, porting a completed Dedekind-zeta construction.

Results

For every number field K, unconditionally, J_{K,d} is nonzero and has at least d − C_K√(d log d) distinct negative real zeros for all large d, so the proportion of real zeros tends to one. The Lean development also establishes the Riemann case for every d ≥ 2 and is available at github.com/AxiomMath/RiemannJensen.