Formal target: Corpus.OEIS179537.conjecture1

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

Exact formal statement

∀ (p : Nat) [Fact (Nat.Prime p)],
  Ne.{1} p 7 →
    Eq.{1} (legendreSym 7 (Nat.cast.{0} p)) 1 →
      ∀ (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} 7 (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 =>
              HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} (-1) k) (Corpus.OEIS179537.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