{"id":"palomar/PALOMAR-2026-10-21-000005","url":"https://github.com/sthubbar/goldbach-lean/tree/6d7ae7b40fb5550e836456fd2ff4d8587157aee7/entries/heathbrown1985","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-21-000005-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11P32","msc:11N13","msc:11M20","msc:11P55","additive-number-theory","goldbach-problem","ternary-goldbach","lean-formalization"],"score":0,"title":"Vinogradov's three primes theorem and almost all binary Goldbach, after Heath-Brown 1985, with the Siegel-Walfisz theorem","trust":"high","domain":"math.NT","source":"palomar","authors":["Steve Hubbard"],"reviews":0,"subject":"math.NT","summary":"A sorry-free Lean 4 proof of the main results of D. R. Heath-Brown, The ternary Goldbach problem, Rev. Mat. Iberoam. 1 (1985): the Siegel-Walfisz theorem in the form the paper quotes as (1.1), proved from a zero-free region for Dirichlet L-functions and Siegel's theorem; Theorem 1, sum over 2x < m <= 3x of |N2(m) - x S(m)| << x^2 (log x)^{-C}; Corollary 1 and the van der Corput, Chudakov, Estermann theorem that at most O(X (log X)^{-A}) even numbers up to X are not sums of two primes, and density zero; Corollary 2, Vinogradov's theorem that every sufficiently large odd number is a sum of…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-21","reactions":{},"formalized":true,"formalizes":[{"title":"The ternary Goldbach problem","identifier":"doi:10.4171/RMI/2","relationship":"formalizes"}]}