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
[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) → Filter.Tendsto (fun x => 1 / ↑x * ∑ n ∈ Finset.Icc 1 x, Erdos377.sumInvPrimesNotDvdCentralBinom n ^ 2) Filter.atTop (nhds (γ₀ ^ 2))SolvedStatement only, no proof