{"id":"palomar/PALOMAR-2026-10-18-000018","url":"https://github.com/AItoBit/erdos-685-elementary-lower-bound/tree/c8618095373664c5c8ea35f78304abdd4ec41691","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000018-v1.json","repo":"https://github.com/AItoBit/erdos-685-elementary-lower-bound","tags":["math.NT","msc:11B65","msc:11A51","number-theory","central-binomial","lean"],"score":0,"title":"Distinct prime divisors of central binomial coefficients","trust":"high","domain":"math.NT","source":"palomar","authors":["AItoBit"],"reviews":0,"subject":"math.NT","summary":"A formal proof of the classical asymptotic omega(binomial(2n,n)) times log n divided by n tending to log 4. The proof combines prime-power estimates, central-binomial bounds, a prime-factor cutoff, and elementary logarithmic limits; it does not use the prime number theorem. This strengthens the earlier finite lower-bound package to a full asymptotic theorem. It does not solve the uniform conjecture in Erdos problem 685 and claims no new mathematical theorem.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"Binomial Coefficients and the Distribution of the Primes","identifier":"https://arxiv.org/abs/0709.4676v1","relationship":"formalizes"}]}