What is the conjecture

Gourevitch's conjecture states an identity between an infinite series involving central binomial coefficients and a constant multiple of $\pi^3$. Specifically, for the infinite series with numerators given by the polynomial $1 + 14n + 76n^2 + 168n^3$ and denominators involving $n$ times the seventh power of the central binomial coefficient $\binom{2n}{n}$, the sum equals $\frac{32}{\pi^3}$: $$\sum_{n=0}^{\infty} \frac{1 + 14n + 76n^2 + 168n^3}{2^{20n}} \cdot \binom{2n}{n}^7 = \frac{32}{\pi^3}$$

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

Sources:

• Jesús Guillera, "About a New Kind of Ramanujan-Type Series," Experimental Mathematics, Volume 12, Issue 4, pages 507–510 (2003). DOI: 10.1080/10586458.2003.10504518. https://eudml.org/doc/52183

Prerequisites needed

Formalizability Rating: 1/5 (0 is best) (as of 2026-01-21)

Mathlib provides strong support for series, summation, and binomial coefficients. The core infrastructure for infinite series (tsum), central binomial coefficients, and real/rational arithmetic exists.

AMS categories

• ams-33
• ams-40
• ams-11

Choose either option

• I plan on adding this conjecture to the repository
• This issue is up for grabs: I would like to see this conjecture added by somebody else

Created by AI, reviewed by me.