{"id":"palomar/PALOMAR-2026-10-22-000023","url":"https://github.com/sthubbar/goldbach-lean/tree/3ba1189ed38f0a913828af00d72196eebd68777f/entries/goldstonyang2016","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000023-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11P32","msc:11M26","msc:11N05","number-theory","goldbach-conjecture","lean-formalization","prime-numbers"],"score":0,"title":"Conditional on RH: the Cesàro average of the number of Goldbach representations, after Goldston and Yang","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 2 of D. A. Goldston and L. Yang, The average number of Goldbach representations, arXiv 1601.06902, in Prime numbers and representation theory, Science Press 2017. 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 zero sum counts zeros with multiplicity, and its absolute convergence is proved unconditionally. Binary Goldbach is open and is not claimed; this is an average over n. An AI agent…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"The average number of Goldbach representations","identifier":"arXiv:1601.06902","relationship":"formalizes"}]}