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

The question

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

• _Zhi-Wei Sun_, Jul 01 2010

conjecture2. If $p$ is a prime with $p\equiv 3,7(\mathrm{mod}20)$ and $2p=x^2+5y^2$ with $x,y$ integers, then ${\sum }_{k=0}^{p-1}a(k)\equiv 2x^2-2p(\mathrm{mod}{p}^2)$.

• _Zhi-Wei Sun_, Jul 01 2010

conjecture3. If $p$ is a prime with $p\equiv 11,13,17,19(\mathrm{mod}20)$, then ${\sum }_{k=0}^{p-1}a(k)\equiv 0(\mathrm{mod}{p}^2)$.

• _Zhi-Wei Sun_, Jul 01 2010

conjecture4. ${\sum }_{k=0}^{n-1}(20k+17)a(k)\equiv 0(\mathrm{mod}n)$ for all $n=1,2,3,\dots$.

• _Zhi-Wei Sun_, Jul 01 2010

conjecture5. ${\sum }_{k=0}^{p-1}(20k+17)a(k)\equiv p(10(-1/p)+7)(\mathrm{mod}{p}^2)$ for any odd prime $p$.

• _Zhi-Wei Sun_, Jul 01 2010

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

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.OEIS.«179524» (5 statements).

theorem conjecture1 (p : ℕ) (hp : p.Prime)
    (h_mod : (p : ℤ) ≡ 1 [ZMOD 20] ∨ (p : ℤ) ≡ 9 [ZMOD 20])
    (x y : ℤ) (h_sq : (p : ℤ) = x ^ 2 + 5 * y ^ 2) :
    ∑ k ∈ Finset.range p, a k ≡ 4 * x ^ 2 - 2 * (p : ℤ) [ZMOD (p : ℤ) ^ 2]

theorem conjecture2 (p : ℕ) (hp : p.Prime)
    (h_mod : (p : ℤ) ≡ 3 [ZMOD 20] ∨ (p : ℤ) ≡ 7 [ZMOD 20])
    (x y : ℤ) (h_sq : 2 * (p : ℤ) = x ^ 2 + 5 * y ^ 2) :
    ∑ k ∈ Finset.range p, a k ≡ 2 * x ^ 2 - 2 * (p : ℤ) [ZMOD (p : ℤ) ^ 2]

theorem conjecture3 (p : ℕ) (hp : p.Prime)
    (h_mod : (p : ℤ) ≡ 11 [ZMOD 20] ∨ (p : ℤ) ≡ 13 [ZMOD 20] ∨
      (p : ℤ) ≡ 17 [ZMOD 20] ∨ (p : ℤ) ≡ 19 [ZMOD 20]) :
    ∑ k ∈ Finset.range p, a k ≡ 0 [ZMOD (p : ℤ) ^ 2]

theorem conjecture4 (n : ℕ) (hn : 1 ≤ n) :
    (n : ℤ) ∣ ∑ k ∈ Finset.range n, ((20 * (k : ℤ) + 17) * a k)

theorem conjecture5 (p : ℕ) [hp : Fact p.Prime] (_hp2 : p ≠ 2) :
    (∑ k ∈ Finset.range p, ((20 * (k : ℤ) + 17) * a k)) ≡
      (p : ℤ) * (10 * legendreSym p (-1) + 7) [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

• A179524
• 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.