Erdős problem 1060
The conjecture is about the function which counts the number of solutions to , where is the sum of divisors of . The first bound is that grows slower than any power of . The second bound is that is at most a power of .
Sources
FormalConjectures/ErdosProblems/
1060.lean
Retained formal statement
Part (ii) of Erdős Problem 1060: bound on the number of with .
∃ C, (fun n => ↑{k ∈ Finset.Iic n | k * (ArithmeticFunction.sigma 1) k = n}.card) =O[Filter.atTop] fun n => Real.log ↑n ^ COpenStatement only, no proof