Bellard's exotic formula for $\pi$

In his webpage, Fabrice Bellard mentions an exotic formula for $\pi$ as follows $$\pi = \frac{1}{740025}\left(\sum_{n = 1}^{\infty}\dfrac{3P(n)}{{\displaystyle \binom{7n}{2n}2^{n - 1}}} - 20379280\right)\tag{1}$$ where \begin{align} P(n) = &-885673181n^{5} + 3125347237n^{4} -2942969225n^{3}\notag\\ &+1031962795n^{2} - 196882274n + 10996648\notag \end{align} and he further adds that this was obtained while testing some numerical relations with PSLQ Algorithm which is a kind of integer relation algorithm.

My point here is not to ask a proof of the formula $(1)$ because it is based on a computer algorithm, but rather to understand how can be we be so sure of accuracy of such formulas obtained via these algorithms unless we have some other proof based on analytical arguments. Fundamentally a computer algorithm can't operate on a real number. The most we can hope for is operations on algebraic numbers. To deal with arbitrary real numbers one does not need "arbitrary precision arithmetic" but rather "infinite precision arithmetic" which is kind of impossible to achieve via computers.

How does one guarantee a computer generated formula like $(1)$ involving transcendental numbers ($\pi$) to be true?

Update: Just so as to highlight the computer based calculations done for algebraic numbers I refer to my answer regarding a Ramanujan's formula for $\pi$.

Solution 1:

At some point you need to tell the computer what $\pi$ is. One option is to give an integral representation: for example, you might tell the computer that

$$\frac{\pi}{4} = \int_0^1 \sqrt{1 - x^2} \, dx.$$

From here, the computer can try to prove statements about $\pi$ by manipulating the integral on the right. For example, $\sqrt{1 - x^2}$ has a power series expansion

$$\sqrt{1 - x^2} = \sum_{n=0}^{\infty} { \frac{1}{2} \choose n } (-1)^n x^{2n}$$

and integrating this power series expansion term by term gives

$$\frac{\pi}{4} = \sum_{n=0}^{\infty} {\frac{1}{2} \choose n} \frac{(-1)^n}{2n+1}.$$

See, that wasn't so hard! Even a computer could've done it. Computers are in fact quite good at manipulating expressions like these formally, and can rigorously prove many things about them; see, for example, Petkovsek, Wilf, and Zeilberger's A=B.

There are no issues involving infinite precision because the computer is not at any point attempting to evaluate the numerical value of both sides or anything like that; instead, it's starting from a fact we tell it about $\pi$ and formally deducing other facts about $\pi$ from it. (I mean, I don't know how to compute $\pi$ to infinite precision, but that's never stopped me from proving facts about $\pi$, and I think anything I can do, a computer could in principle do.)

Edit: Okay, so I actually read a little about the PSLQ algorithm. It does not prove anything: as far as I can tell, what it actually does is give a very clever way to guess integer relations between real numbers which you provide it by providing a very large number of their digits. Once you have such a guess, you can verify it to as high a precision as you want by computing more digits. That's not a proof, but it's very good evidence, and the more digits you compute the better evidence it is. Then you can look for a proof.

Solution 2:

(Too long for a comment.)

In fact, for order $m=7$, we have,

$$740025\pi+20379280 = \sum_{n=1}^\infty \dfrac{3P_1(n)}{{\displaystyle \tbinom{7n}{2n}2^{n-1}}}\tag1$$

$$740025\pi+19755520 = \sum_{n=1}^\infty \dfrac{P_2(n)}{{\displaystyle \tbinom{7n}{2n}2^{n-1}}}\tag2$$

$$740025\pi+18776800 = \sum_{n=1}^\infty \dfrac{P_3(n)}{{\displaystyle \tbinom{7n}{2n}2^{n-1}}}\tag3$$

where,

$$\small{P_1(n) = 10996648 - 196882274 n + 1031962795 n^2 - 2942969225 n^3 + 3125347237 n^4 - 885673181 n^5}$$

$$\small{P_2(n) = 20202864 - 361815268 n + 1669902852 n^2 - 4185508285 n^3 + 1811392311 n^4 + 3820998353 n^5 - 2124144507 n^6}$$

$$\small{P_3(n) = 11290944 - 204904056 n + 859781414 n^2 - 2018500197 n^3 + 403088421 n^4 + 2078563631 n^5 + 1880241301 n^6 - 1808396978 n^7}$$

and so on (apparently).

In this paper, the authors relate pi formulas of this form to some integral. However, it doesn't seem to be explored that there might be multiple $P(n)$ of different degrees that can be used as a numerator.