Formal target: Corpus.OEIS141057.conjecture1

Conjecture: the supercongruences $a(n \cdot p^k) \equiv a(n \cdot p^{k-1}) \pmod{p^{3k}}$ hold for primes $p \ge 5$ and positive integers $n$ and $k$.

Exact formal statement

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

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record