Erdős problem 1000
Let be an infinite sequence of integers, and let count the number of such that the fraction does not have denominator for when written in lowest form; equivalently, for all .
Sources
FormalConjectures/ErdosProblems/
1000.lean
Retained formal statement
Erdős [Er64b] proved that the limit of as cannot be .
∀ (n : ℕ → ℕ), StrictMono n → 0 < n 0 → ¬Filter.Tendsto (fun k => ↑(Erdos1000.phiSeq n k) / ↑(n k)) Filter.atTop (nhds 0)SolvedStatement only, no proof