{"id":"palomar/PALOMAR-2026-10-22-000025","url":"https://github.com/sthubbar/goldbach-lean/tree/559706d617bc554787e10dba07066dc63ab69cb5/entries/languascozaccagnini2012","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000025-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11P32","msc:11M26","msc:11N05","number-theory","goldbach-conjecture","lean-formalization","analytic-number-theory"],"score":0,"title":"Conditional on RH: the number of Goldbach representations on average, after Languasco and Zaccagnini","trust":"high","domain":"math.NT","source":"palomar","authors":["Steve Hubbard"],"reviews":0,"subject":"math.NT","summary":"Conditional on RH: a sorry-free Lean 4 proof of Theorem 1 of A. Languasco and A. Zaccagnini, The number of Goldbach representations of an integer, Proc. Amer. Math. Soc. 140 2012, 795 to 804. With G(n) the sum over m1 + m2 = n of Lambda(m1) Lambda(m2), Mathlib's RiemannHypothesis, taken as an explicit hypothesis of the theorem and never as an axiom, implies that the sum over n = 2. The weaker earlier error terms of Fujii, O((N log N)^{4/3}), and of Bhowmik and Schlage-Puchta, O(N log^5 N), follow and are stated too. The zero sum counts zeros with multiplicity, and its absolute convergence is…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"The number of Goldbach representations of an integer","identifier":"arXiv:1011.3198","relationship":"formalizes"},{"title":"An additive problem of prime numbers. II","identifier":"Proc. Japan Acad. Ser. A Math. Sci. 67, 1991, 248-252","relationship":"formalizes"},{"title":"Mean representation number of integers as the sum of primes","identifier":"arXiv:0806.3295","relationship":"formalizes"}]}