{"id":"palomar/PALOMAR-2026-10-27-000008","url":"https://github.com/sthubbar/goldbach-lean/tree/df67596bfcac1741523a833d302d39f1823837a4/entries/alsetrishao2024","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-27-000008-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11P32","msc:11B30","msc:11N13"],"score":0,"title":"A density version of the binary Goldbach problem, after Alsetri and Shao","trust":"high","domain":"math.NT","source":"palomar","authors":["Steve Hubbard"],"reviews":0,"subject":"math.NT","summary":"A sorry-free Lean 4 proof, with no cited hypothesis, of Theorem 1.2 of A. Alsetri and X. Shao, Density versions of the binary Goldbach problem, arXiv 2405.18576v2, Acta Arith. 218, 2025, 285 to 295: if A is a set of primes whose relative lower density in every reduced residue class b mod W is at least some eta > 1/2, then almost all even positive integers are a sum of two primes from A. The entry also proves the paper's Theorem 1.1, that relative density 1 - epsilon in the primes alone does not suffice, and the sharpness of the constant 1/2 stated in its Remark 1.3. A derived result of this…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-27","reactions":{},"formalized":true,"formalizes":[{"title":"Density versions of the binary Goldbach problem","identifier":"arXiv:2405.18576","relationship":"formalizes"}]}