Number theory

Erdős 1060 - part ii

Part (ii) of Erdős Problem 1060: bound on the number of

k \le n

with

k \sigma_1(k) = n

References

erdosproblems.com/1060

No one has attempted this yet.

Formal statement

Lean type

∃ C,
  (fun n => ↑{k ∈ Finset.Iic n | k * (ArithmeticFunction.sigma 1) k = n}.card) =O[Filter.atTop] fun n => Real.log ↑n ^ C

What you must prove

import FormalConjectures.ErdosProblems.«1060»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos1060.erdos_1060.parts.ii" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/1060.lean

Source type SHA-256: sha256:54f3b7b4b823bc8a18df4ae05c4ab1de33341861f66042fd8c0818a59f1b053c
Task id: fc-379fc029-parts-ii-f23756df5a-formalized-v1
Task commitment: sha256:5f767e8f4a5bab7bcffa53a47d8b9be9cf519268889a597d77a9361d7e85a0dc

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.