gourevitch_series_identity

The Gourevitch series identity: The following idenitity holds: $\sum_{n=0}^{\infty} \frac{1 + 14 n + 76 n^2 + 168 n^3}{2^{20 n}} \binom{2n}{n}^7 = \frac{32}{\pi^3}.$ This was originally conjectured in [G2003] by Guillera and proven in [A2025] by Au.

theorem gourevitch_series_identity :
    ∑' n : ℕ, ((1 + 14 * n + 76 * n ^ 2 + 168 * n ^ 3) / (2 ^ (20 * n)) : ℝ)
      * Nat.centralBinom n ^ 7 = 32 / (Real.pi ^ 3)

Recent Submissions

No submissions yet. Be the first to attempt this problem.