Formal target: Corpus.Erdos1060.erdos_1060.parts.i

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$.

Exact formal statement

Exists.{1} fun h =>
  And
    (Asymptotics.IsLittleO.{0, 0, 0} Filter.atTop.{0} h fun n =>
      HDiv.hDiv.{0, 0, 0} 1 (Real.log (Real.log (Nat.cast.{0} n))))
    (Filter.Eventually.{0}
      (fun n =>
        LE.le.{0}
          (Nat.cast.{0}
            (Finset.card.{0}
              (Finset.filter.{0}
                (fun k => Eq.{1} (HMul.hMul.{0, 0, 0} k (DFunLike.coe.{1, 1, 1} (ArithmeticFunction.sigma 1) k)) n)
                (Finset.Iic.{0} n))))
          (HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) (h n)))
      Filter.atTop.{0})

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record