Brun's theorem: the sum of the reciprocals of the twin primes converges, after Brun 1919, with the twin prime upper bound and every even gap
A sorry-free Lean 4 proof of the theorem of V. Brun, La série 1/5 + 1/7 + 1/11 + 1/13 + ... où les dénominateurs sont nombres premiers jumeaux est convergente ou finie, Bull. Sci. Math. 43, 1919: the sum of the reciprocals of p and of p + 2 over the primes p with p + 2 prime converges. This is a sorry-free proof of a statement that lean-eval lists as a challenge, brun_constant_converges, proved here in the exact lean-eval form as well. With it, the twin prime upper bound, at most C N / log^2 N twin primes below N, which is stronger than the bound of Brun's paper; the same convergence for…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000003/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-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'