{"id":"palomar/PALOMAR-2026-10-22-000028","url":"https://github.com/sthubbar/goldbach-lean/tree/4d87394fed5e86a866ec2335621dc1b57f2e0c9d/entries/renyi1948","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-22-000028-v1.json","repo":"https://github.com/sthubbar/goldbach-lean","tags":["math.NT","msc:11P32","msc:11N35","msc:11N36","number-theory","prime-numbers","lean-formalization","almost-primes"],"score":0,"title":"Renyi's theorem, Renyi 1948: every large even number is a prime plus a number with at most 8 prime factors","trust":"high","domain":"math.NT","source":"palomar","authors":["Steve Hubbard"],"reviews":0,"subject":"math.NT","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-22","reactions":{},"formalized":true,"formalizes":[{"title":"On the representation of an even number as the sum of a single prime and a single almost-prime number","identifier":"https://www.mathnet.ru/eng/im3018","relationship":"adapts"}]}