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
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 .
∃ h, (h =o[Filter.atTop] fun n => 1 / Real.log (Real.log ↑n)) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑{k ∈ Finset.Iic n | k * (ArithmeticFunction.sigma 1) k = n}.card ≤ ↑n ^ h nOpenStatement only, no proof