Erdős problem 377
Is there some absolute constant such that for all ?
Sources
FormalConjectures/ErdosProblems/
377.lean
Retained formal statement
Erdos, Graham, Ruzsa, and Straus proved that if then there is some constant such that for all large
[EGRS75] Erdős, P. and Graham, R. L. and Ruzsa, I. Z. and Straus, E. G., _On the prime factors of _. Math. Comp. (1975), 83-92.
∃ c < 1, ∀ᶠ (n : ℕ) in Filter.atTop, Erdos377.sumInvPrimesNotDvdCentralBinom n ≤ c * Real.log (Real.log ↑n)SolvedStatement only, no proof