Formal target: Corpus.OEIS2326.conjecture1

If $p$ is an odd prime then $a((p^3-1)/2) = p \cdot a((p^2-1)/2)$.

Exact formal statement

∀ (p : Nat),
  Nat.Prime p →
    Ne.{1} p 2 →
      Eq.{1} (Corpus.OEIS2326.a (HDiv.hDiv.{0, 0, 0} (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} p 3) 1) 2))
        (HMul.hMul.{0, 0, 0} p
          (Corpus.OEIS2326.a (HDiv.hDiv.{0, 0, 0} (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} p 2) 1) 2)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record