Formal target: Corpus.OEIS179524.conjecture1

If $p$ is a prime with $p \equiv 1, 9 \pmod{20}$ and $p = x^2 + 5y^2$ with $x, y$ integers, then $\sum_{k=0}^{p-1} a(k) \equiv 4x^2 - 2p \pmod{p^2}$.

Exact formal statement

∀ (p : Nat),
  Nat.Prime p →
    Or (Int.ModEq 20 (Nat.cast.{0} p) 1) (Int.ModEq 20 (Nat.cast.{0} p) 9) →
      ∀ (x y : Int),
        Eq.{1} (Nat.cast.{0} p)
            (HAdd.hAdd.{0, 0, 0} (HPow.hPow.{0, 0, 0} x 2) (HMul.hMul.{0, 0, 0} 5 (HPow.hPow.{0, 0, 0} y 2))) →
          (HPow.hPow.{0, 0, 0} (Nat.cast.{0} p) 2).ModEq
            (Finset.sum.{0, 0} (Finset.range p) fun k => Corpus.OEIS179524.a k)
            (HSub.hSub.{0, 0, 0} (HMul.hMul.{0, 0, 0} 4 (HPow.hPow.{0, 0, 0} x 2))
              (HMul.hMul.{0, 0, 0} 2 (Nat.cast.{0} p)))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record