Schnirelmann's theorem: every integer n >= 2 is a sum of at most 30772 primes, after Schnirelmann 1933
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000005
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000005/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000005/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'