{"id":"palomar/PALOMAR-2026-08-25-000005","url":"https://github.com/teal-sea/zeta-lab/tree/84312e4477dfeb7e0d8a91c38897f225f5a52f19/lean/bridge","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-25-000005-v1.json","repo":"https://github.com/teal-sea/zeta-lab","tags":["math.NT","msc:11M26","msc:15A42","riemann-zeta","number-theory","lean","zeros"],"score":0,"title":"teal-sea/zeta-lab","trust":"high","domain":"math.NT","source":"palomar","authors":["Thomas Lince"],"reviews":0,"subject":"math.NT","summary":"Let N(T,2T) count the nontrivial zeros of the Riemann zeta function with ordinate in (T,2T], with multiplicity, and N_0^s(T,2T) the simple zeros among them on the critical line. The Lean development accompanying arXiv:2608.13637 (anthropics/zeta-23-lean) proves, for Mathlib's riemannZeta and unconditionally, that for every eps > 0 and all large T, (H - eps) N(T,2T) = 2, c > 0, m >= n, p > 0 with c(m-(n-1)) 0 and all large T, (Phi_n(n,c,m,p) - eps) N(T,2T) <= N_0^s(T,2T), where Phi_n(n,c,m,p) = (H - (n-1)(m-1)/(pm)) / (1 - c(m-(n-1))/m). At n = 7 this is Ainta's theorem. THE THREE-POINT…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-25","reactions":{},"formalized":true,"formalizes":[{"title":"More than 67.3% of the zeros of the Riemann zeta function are simple and lie on the critical line","identifier":"","relationship":"adapts"}]}