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 .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/1060.lean∃ 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