Erdős problem 1060

The conjecture is about the function $f(n)$ which counts the number of solutions to $k\sigma(k)=n$ , where $\sigma(k)$ is the sum of divisors of $k$ . The first bound is that $f(n)$ grows slower than any power of $n^(\frac{1}{\log\log n})$ . The second bound is that $f(n)$ is at most a power of $\log n$ .

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1060.lean

Retained formal statement1 of 2

The conjecture is about the function $f(n)$ which counts the number of solutions to $k\sigma(k)=n$ , where $\sigma(k)$ is the sum of divisors of $k$ . The first bound is that $f(n)$ grows slower than any power of $n^(\frac{1}{\log\log n})$ . The second bound is that $f(n)$ is at most a power of $\log n$ .

FormalConjectures/ErdosProblems/1060.leanErdos1060.erdos_1060.parts.i3 linesExact file

1∃ h,2  (h =o[Filter.atTop] fun n => 1 / Real.log (Real.log ↑n)) ∧3    ∀ᶠ (n : ℕ) in Filter.atTop, ↑{k ∈ Finset.Iic n | k * (ArithmeticFunction.sigma 1) k = n}.card ≤ ↑n ^ h n

OpenStatement only, no proof