Erdős problem 489
If is a forbidden-divisor set with and the sifted set, must converge to a finite limit?
Sources
FormalConjectures/ErdosProblems/
489.lean
Retained formal statement
When , is the set of squarefree numbers, and the existence of this limit was proved by Erdős. This is the case of Erdős Problem 145.
∃ L, Filter.Tendsto (fun x => Erdos489.GapSumSq {n | ∃ p, Nat.Prime p ∧ n = p ^ 2} x / ↑x) Filter.atTop (nhds L)SolvedStatement only, no proof