Formal target: Corpus.OEIS3162.conjecture

Let $b(n) = a(2n-1)$.

Exact formal statement

∀ (n k p : Nat),
  LT.lt.{0} 0 n →
    LT.lt.{0} 0 k →
      Nat.Prime p →
        LE.le.{0} 5 p →
          (HPow.hPow.{0, 0, 0} (Nat.cast.{0} p) (HMul.hMul.{0, 0, 0} 3 k)).ModEq
            (Corpus.OEIS3162.b (HMul.hMul.{0, 0, 0} n (HPow.hPow.{0, 0, 0} p k))).num
            (Corpus.OEIS3162.b (HMul.hMul.{0, 0, 0} n (HPow.hPow.{0, 0, 0} p (HSub.hSub.{0, 0, 0} k 1)))).num

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record