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 .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/1000.leanTrue ↔ ∃ n, StrictMono n ∧ 0 < n 0 ∧ Filter.Tendsto (Erdos1000.phiAvg n) Filter.atTop (nhds 0)Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:1000 - PLBY Lean proofs
ErdosProblems.Erdos1000
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine