{"id":"palomar/PALOMAR-2026-10-22-000005","url":"https://github.com/sthubbar/goldbach-lean/tree/3ba1189ed38f0a913828af00d72196eebd68777f/entries/schnirelmann1933","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000005-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11P32","msc:11B13","msc:11N36","number-theory","additive-combinatorics","formal-verification","lean"],"score":0,"title":"Schnirelmann's theorem: every integer n >= 2 is a sum of at most 30772 primes, after Schnirelmann 1933","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 L. Schnirelmann, Über additive Eigenschaften von Zahlen, Math. Ann. 107, 1933: the set of 0, 1 and the sums of two primes has positive Schnirelmann density, and so every integer n >= 2 is a sum of a bounded number of primes. The proof also gives an explicit bound: every n >= 2 is a sum of at most 30772 primes. Mathlib's file Mathlib/Combinatorics/Schnirelmann.lean lists the proof of Schnirelmann's theorem as a TODO; this entry gives it, for Mathlib's schnirelmannDensity, with an explicit constant. The constant 30772 is far weaker than…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"Über additive Eigenschaften von Zahlen","identifier":"doi:10.1007/BF01448914","relationship":"formalizes"},{"title":"Additive Number Theory: The Classical Bases","identifier":"doi:10.1007/978-1-4757-3845-2","relationship":"adapts"},{"title":"On Šnirel'man's constant","identifier":"https://numdam.org/item/ASNSP_1995_4_22_4_645_0/","relationship":"adapts"}]}