Erdős problem 448
Let count the divisors of and count the number of such that has a divisor in . Is it true that, for all , for almost all ?
Sources
FormalConjectures/ErdosProblems/
448.lean
Retained formal statement
A more precise result of Hall and Tenenbaum [HaTe88, §4.6]: the upper density of is as .
(fun ε => {n | ↑(Erdos448.tauPlus n) < ε * ↑n.divisors.card}.upperDensity) =O[nhdsWithin 0 (Set.Ioi 0)] fun ε => ε * Real.log (2 / ε)SolvedStatement only, no proof