Mann's alpha plus beta theorem for Schnirelmann density, after Mann 1942
A Lean 4 proof, with no unproved steps, of the theorem of H. B. Mann, A proof of the fundamental theorem on the density of sums of sets of positive integers, Ann. of Math. 43, 1942: for sets A and B of natural numbers that contain 0, the Schnirelmann density of A + B is at least the minimum of 1 and sigma A + sigma B. It is stated for Mathlib's own schnirelmannDensity and Mathlib's pointwise sum of sets, so the Challenge restates no density definition, and it is also proved for any finite number of sets. This fills a Mathlib TODO: Mathlib/Combinatorics/Schnirelmann.lean lists Mann's theorem…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000024
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000024/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-000024/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'