{"id":"palomar/PALOMAR-2026-10-22-000002","url":"https://github.com/sthubbar/goldbach-lean/tree/5a11b2651e31507826f7423efbfa4e2d4d42a89f/entries/romanov1934","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000002-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11P32","msc:11B05","msc:11N36","additive-number-theory","primes","covering-systems","lean"],"score":0,"title":"Romanov's theorem: the integers of the form p + 2^k have positive lower density, with Erdős' complement, after Romanov 1934 and Erdős 1950","trust":"high","domain":"math.NT","source":"palomar","authors":["Steve Hubbard"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 proof, with no unproved steps, of the theorem of N. P. Romanov, Über einige Sätze der additiven Zahlentheorie, Math. Ann. 109, 1934: the integers p + 2^k, p prime, have positive lower density, for k >= 0 and for k >= 1. With it, the result of P. Erdős, On integers of the form 2^k + p and some related problems, Summa Brasil. Math. 2, 1950: by a covering system, every 119477317 + 346729110 t is odd and is not p + 2^k, so the odd numbers that are not of that form also have positive lower density. Binary Goldbach is open and is not claimed. The Lean code was written by an AI agent and…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Über einige Sätze der additiven Zahlentheorie","identifier":"doi:10.1007/BF01449161","relationship":"formalizes"},{"title":"On integers of the form 2^k + p and some related problems","identifier":"Summa Brasiliensis Mathematicae 2, 1950, pages 113-123","relationship":"adapts"}]}