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
Sanity check: . Divisors lie in dyadic blocks , so the distinct blocks are . (.)
Erdos448.tauPlus 6 = 3TestStatement only, no proof