Formal target: Corpus.OEIS38098.conjecture1

Conjecture (i): for any integer $k > 2$, the sequence $\pi(n^k)/n^k$ ($n = 2, 3, \ldots$) is strictly decreasing, where $\pi(x)$ denotes the number of primes not exceeding $x$.

Exact formal statement

∀ (k : Nat),
  LT.lt.{0} 2 k →
    ∀ (n : Nat),
      LE.le.{0} 2 n →
        LT.lt.{0}
          (HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (HPow.hPow.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} n 1) k).primeCounting)
            (HPow.hPow.{0, 0, 0} (HAdd.hAdd.{0, 0, 0} (Nat.cast.{0} n) 1) k))
          (HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (HPow.hPow.{0, 0, 0} n k).primeCounting)
            (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