Formal target: Corpus.OEIS49473.conjecture

Let $s(n) = \zeta(3) - \sum_{k=1}^n \frac{1}{k^3}$.

Exact formal statement

And
  (∀ (n : Nat),
    LE.le.{0} 1 n →
      And
        (LT.lt.{0} (Corpus.OEIS49473.s (Corpus.OEIS49473.a n))
          (HDiv.hDiv.{0, 0, 0} 1 (HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) 2)))
        (LT.lt.{0} (HDiv.hDiv.{0, 0, 0} 1 (HPow.hPow.{0, 0, 0} (Nat.cast.{0} n) 2))
          (Corpus.OEIS49473.s (HSub.hSub.{0, 0, 0} (Corpus.OEIS49473.a n) 1))))
  (∀ (n : Nat),
    LE.le.{0} 1 n →
      have diff := HSub.hSub.{0, 0, 0} (Corpus.OEIS49473.a n) (Corpus.OEIS49473.a (HSub.hSub.{0, 0, 0} n 1));
      And (Iff (Eq.{1} diff 0) (Membership.mem.{0, 0} Corpus.OEIS49473.A001954 (HSub.hSub.{0, 0, 0} n 1)))
        (Iff (Eq.{1} diff 1) (Membership.mem.{0, 0} Corpus.OEIS49473.A001953 (HSub.hSub.{0, 0, 0} n 1))))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record