Erdős problem 1201
Is it true that for every there exists a such that the density of for which is at least , where is the greatest prime divisor of ? A short argument via the Matomäki-Radziwiłł theorem establishes the lower-density version.
Sources
FormalConjectures/ErdosProblems/
1201.lean
Retained formal statement
Erdős wrote he could prove this for .
∀ η > 0, ∃ k, Filter.liminf (fun x => ↑↑(Nat.count (Erdos1201.Erdos1201Set (1 / 2) k) x) / ↑↑x) Filter.atTop ≥ 1 - ηSolvedStatement only, no proof