Renyi's theorem, Renyi 1948: every large even number is a prime plus a number with at most 8 prime factors
A sorry-free Lean 4 proof of Renyi's theorem: there is N0 such that every even N >= N0 is p + m with p prime, m >= 1 and Omega of m at most 8, where Omega counts prime factors with multiplicity, as Mathlib's ArithmeticFunction.cardFactors does. So the theorem is proved with the explicit constant K = 8. Also proved: a lower bound e^{-36} N / 2 log^2 N for the number of primes p < N with Omega of N - p at most 8; the same two statements with the weaker K = 13000; and the K = 8 statement written with Mathlib's Nat.IsAtMostAlmostPrime. The entry also proves twin_renyi_count, a derived analogue…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-22-000028
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-22-000028/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-000028/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'