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 and then for almost all integers .
[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.
∀ (γ₀ : ℝ), γ₀ = ∑' (k : ℕ), Real.log (↑k + 2) / 2 ^ (k + 2) → ∃ o, ∃ (_ : Filter.Tendsto o Filter.atTop (nhds 0)), ∀ᶠ (n : ℕ) in Filter.cofinite, Erdos377.sumInvPrimesNotDvdCentralBinom n = γ₀ + o nSolvedStatement only, no proof