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
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 .
Is there a sequence such that
This was solved by Haight [Ha] who proved that such a sequence does exist (contrary to Erdős' expectations).
True ↔ ∃ n, StrictMono n ∧ 0 < n 0 ∧ Filter.Tendsto (Erdos1000.phiAvg n) Filter.atTop (nhds 0)