Formal target: Corpus.OEIS357513.general_supercongruence

We conjecture that $u(p-1) == 0 (mod p^4)$ for all primes $p$, with a finite number of exceptions that depend on $m$.

Exact formal statement

∀ (m : Nat),
  Exists.{1} fun exceptions =>
    ∀ (p : Nat),
      Nat.Prime p →
        Not (Membership.mem.{0, 0} exceptions p) →
          Eq.{1} (Nat.cast.{0} (Corpus.OEIS357513.u m (HSub.hSub.{0, 0, 0} p 1))) 0

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record