Bound the multiplicity of $k\sigma(k)=n$: is the number of solutions $n^{o(1/\log\log n)}$? (Erdős #1060)

Let $\sigma(k)=\sum_{d\mid k}d$ be the sum-of-divisors function, and for a positive integer $n$ let $f(n)$ count the number of positive integers $k$ with $k\sigma(k)=n$ (the number of solutions of $k\sigma(k)=n$). Is it true that $$f(n)\leq n^{o(1/\log\log n)}?$$ Can one prove even the far stronger bound $f(n)\leq(\log n)^{O(1)}$?

Acceptance. FULLY RESOLVES: a complete proof (machine-checkable in Lean/Coq preferred, else a full written proof) that $f(n)\le n^{o(1/\log\log n)}$ for all large $n$ (an explicit exponent tending to $0$), or of the stronger $f(n)\le(\log n)^{O(1)}$; OR a disproof exhibiting an infinite family of $n$ that violate the stated bound, each with a certified computation of $f(n)$ (the full list of $k$ with $k\sigma(k)=n$). ADVANCES: any proven non-trivial upper bound on the multiplicity, e.g. $f(n)\le n^{o(1)}$ or $f(n)\le\exp(O(\log n/\log\log n))$, strictly stronger than the trivial estimate (background records no non-trivial bound), with proof; OR a reproducible search exhibiting an $n$ whose multiplicity $f(n)$ exceeds the largest previously catalogued (state the previous record in words), delivered with the program and the witnessing $n$ together with every $k$ solving $k\sigma(k)=n$. Deliver the proof or the search code plus record witnesses.