Formal target: Corpus.OEIS1157.conjecture

Conjecture: For each k = 2,3,..., all the rational numbers $\frac{\sigma_k(n)}{n^k} = \sum_{d|n} \frac{1}{d^k}$ (n = 1,2,3,...) have pairwise distinct fractional parts.

Exact formal statement

∀ (k : Nat),
  LE.le.{0} 2 k →
    ∀ (n₁ n₂ : Nat),
      LT.lt.{0} 0 n₁ →
        LT.lt.{0} 0 n₂ →
          Ne.{1} n₁ n₂ →
            Ne.{1}
              (Int.fract.{0}
                (HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (DFunLike.coe.{1, 1, 1} (ArithmeticFunction.sigma k) n₁))
                  (HPow.hPow.{0, 0, 0} (Nat.cast.{0} n₁) k)))
              (Int.fract.{0}
                (HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (DFunLike.coe.{1, 1, 1} (ArithmeticFunction.sigma k) n₂))
                  (HPow.hPow.{0, 0, 0} (Nat.cast.{0} n₂) k)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record