{"id":"palomar/PALOMAR-2026-10-07-000009","url":"https://github.com/mrklwk/zeta-zero-density-lean/tree/5dd0dd391c117ef4d8fd04a6b16b4b1ad5735d88/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-07-000009-v1.json","repo":"https://github.com/mrklwk/zeta-zero-density-lean","tags":["math.NT","msc:11M26","analytic-number-theory","riemann-zeta","lean-formalization"],"score":0,"title":"The density hypothesis for σ > 3/4","trust":"high","domain":"math.NT","source":"palomar","authors":["Mark Lewko"],"reviews":0,"subject":"math.NT","summary":"Lean formalization of Nζ(σ,T) ≪σ,ε T^(2(1−σ)+ε), hence A(σ) ≤ 2, for fixed 3/4 0; zeros with Re(ρ) ≥ σ and 0 < Im(ρ) ≤ T are counted with multiplicity.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-07","reactions":{},"formalized":true,"formalizes":[{"title":"Unpublished proof notes on large values and zeta zero density","identifier":"","relationship":"formalizes"}]}