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
Always : the occupied dyadic blocks are the image of the divisor set under Nat.log 2, and an image has at most as many elements as its source. This is what makes the comparison in the problem meaningful.
∀ (n : ℕ), Erdos448.tauPlus n ≤ n.divisors.cardTestStatement only, no proof