Central binomial sum a(n) = Σ_k=0^n C(n, k)^2 C(n-k, k)^2 (-16)^k

The question

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(\mathrm{mod}{p}^2)$.

• _Zhi-Wei Sun_, Jul 17 2010

conjecture2. If $p$ is a prime with $(p/7)=-1$, then ${\sum }_{k=0}^{p-1}(-1{)}^{k}a(k)\equiv 0(\mathrm{mod}{p}^2)$.

• _Zhi-Wei Sun_, Jul 17 2010

conjecture3. ${\sum }_{k=0}^{n-1}(42k+37)(-1{)}^{k}a(k)\equiv 0(\mathrm{mod}n)$ for all $n\ge 1$.

• _Zhi-Wei Sun_, Jul 17 2010

conjecture4. ${\sum }_{k=0}^{p-1}(42k+37)(-1{)}^{k}a(k)\equiv p(21(p/7)+16)(\mathrm{mod}{p}^2)$ for any prime $p\ne 7$.

• _Zhi-Wei Sun_, Jul 17 2010

The sequence is defined by $$a(n)=\sum _{k=0}^n{\left(\genfrac{}{}{0ex}{}{n}{k}\right)}^2{\left(\genfrac{}{}{0ex}{}{n-k}{k}\right)}^2(-16{)}^k.$$

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.OEIS.«179537» (4 statements).

theorem conjecture1 (p : ℕ) [Fact p.Prime] (hp7 : p ≠ 7)
    (h_leg : letI : Fact (Nat.Prime 7) := ⟨by decide⟩; legendreSym 7 p = 1)
    (x y : ℤ) (h_sq : (p : ℤ) = x ^ 2 + 7 * y ^ 2) :
    (∑ k ∈ Finset.range p, (-1 : ℤ) ^ k * a k) ≡
      4 * x ^ 2 - 2 * (p : ℤ) [ZMOD (p : ℤ) ^ 2]

theorem conjecture2 (p : ℕ) [Fact p.Prime] (hp7 : p ≠ 7)
    (h_leg : letI : Fact (Nat.Prime 7) := ⟨by decide⟩; legendreSym 7 p = -1) :
    (∑ k ∈ Finset.range p, (-1 : ℤ) ^ k * a k) ≡ 0 [ZMOD (p : ℤ) ^ 2]

theorem conjecture3 (n : ℕ) (hn : 1 ≤ n) :
    (n : ℤ) ∣ ∑ k ∈ Finset.range n, ((42 * (k : ℤ) + 37) * (-1 : ℤ) ^ k * a k)

theorem conjecture4 (p : ℕ) [Fact p.Prime] (_hp7 : p ≠ 7) :
    letI : Fact (Nat.Prime 7) := ⟨by decide⟩
    (∑ k ∈ Finset.range p, ((42 * (k : ℤ) + 37) * (-1 : ℤ) ^ k * a k)) ≡
      (p : ℤ) * (21 * legendreSym 7 p + 16) [ZMOD (p : ℤ) ^ 2]

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• A179537
• Z.-W. Sun, "Open Conjectures on Congruences", arXiv preprint arXiv:0911.5665 [math.NT], 2009-2011.

Source and licence

Imported from Formal Conjectures (OEIS), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.