{"id":"palomar/PALOMAR-2026-09-23-000001","url":"https://github.com/andrewfiori/ZeroDensityInShortIntervals/tree/97ee4b41d2d4a0680434282e09e688424b59922a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-23-000001-v1.json","repo":"https://github.com/andrewfiori/ZeroDensityInShortIntervals","tags":["math.NT","msc:11M26","msc:11M06","msc:11Y35","msc:68V20","analytic-number-theory","zeta-function","zero-density","lean"],"score":0,"title":"Zero density theorems for short intervals","trust":"high","domain":"math.NT","source":"palomar","authors":["Andrew Fiori"],"reviews":0,"subject":"math.NT","summary":"Explicit zero-density results for the Riemann zeta function in short intervals, formalized in Lean 4 over Mathlib. Count the nontrivial zeros whose imaginary part lies in a window (t-h, t+h], with multiplicity and with a zero on either horizontal edge counted for half. Seven statements are submitted, and all seven are mechanically checked. Two are zero-density bounds for the edge strip Re s > 1-alpha, valid for 0 1 - conj(rho), proved in the development to be a multiplicity-preserving involution of the zero set. The results are conditional and their hypotheses are in the signature, not…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-23","reactions":{},"formalized":true,"formalizes":[{"title":"Zero Density Theorems for Short Intervals","identifier":"arXiv:2609.22624","relationship":"formalizes"}]}