{"id":"palomar/PALOMAR-2026-10-21-000011","url":"https://github.com/sthubbar/goldbach-lean/tree/9cee15bce4cc89532440973263a0f2fe0bd115c0/entries/granville2007","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-21-000011-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11P32","msc:11M26","msc:11N05","number-theory","goldbach","riemann-hypothesis","lean"],"score":0,"title":"The Riemann hypothesis is equivalent to an asymptotic for the average number of Goldbach representations, after Granville 2007","trust":"high","domain":"math.NT","source":"palomar","authors":["Steve Hubbard"],"reviews":0,"subject":"math.NT","summary":"A sorry-free Lean 4 proof of Theorem 1A of A. Granville, Refinements of Goldbach's conjecture, and the generalized Riemann hypothesis, Funct. Approx. Comment. Math. 37 (2007): with G(n) the sum over m1 + m2 = n of Lambda(m1) Lambda(m2), Mathlib's RiemannHypothesis holds if and only if the sum of G(n) over n 0. Both directions are proved with no hypothesis: RH implies the asymptotic through the von Koch bound for psi(x) - x, and the asymptotic implies RH by the route reconstructed in part by Bhowmik, Halupczok, Matsumoto, Suzuki (arXiv 1704.06103) and completed by Bhowmik and Ruzsa (arXiv…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"Refinements of Goldbach's conjecture, and the generalized Riemann hypothesis","identifier":"doi:10.7169/facm/1229618748","relationship":"formalizes"}]}