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)}{\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$.

• You will find a lot of these $\pi$ examples from the works of Ramanujan... – NeilRoy Jun 13 '15 at 6:46
• @NeilRoy: Ramanujan obtained a lot of formulas which can be termed as "exotic", but he obtained them via hand calculation and he had rigorous proofs for all the $\pi$ formulas. He did publish papers on the technique to obtain these formulas, but never gave the details of calculation. See my posts starting from paramanands.blogspot.com/2012/03/… – Paramanand Singh Jun 13 '15 at 7:41
• As a man who has fooled around for several months with numeric approximations of various famous constants, all that I can tell you is that, even if one does not restrict itself to adding up terms of a certain fixed form, even then, in order to build up only a few decimals of precision, one needs to add crazier and crazier terms, and the idea of them being regular is simply out of the question. The coincidence which the rationals involved in your formula could yield, assuming the formula were incorrect or inexact, would not be more than a few decimals, tops. – Lucian Jun 13 '15 at 14:20
• @K.Dutta: I think you are ready for studying work of ramanujan. You can start with Ramanujan Notebooks and my blog posts. – Paramanand Singh Jun 17 '15 at 13:09
• @K.Dutta: If you have any queries you can send comments on my blog. I can reply there. I may not be available for chat on weekdays. – Paramanand Singh Jun 17 '15 at 15:50

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.

• Thanks a lot Qiaochu Yuan. I fully agree with your answer. Also from your edit it means that PSLQ only gives some level of confidence (in fact very high level) that a particular formula may be true, but an actual proof would involve some analytic investigation. +1 – Paramanand Singh Jun 13 '15 at 7:28
• By the way I have the copy of "A=B". I must say its a wonderful book and provides a very different approach to proving identities. – Paramanand Singh Jun 13 '15 at 7:30
• Given how small the numbers are in the expressions and how simple the expressions are inside the summation, shouldn't there be a way of reducing the verification requirement for proof to a, possibly enormous, but finite size? Suppose one tried to create a formula that is almost equal to $\pi$ but not quite -- then, assuming the formula for $\pi$ is "small", producing that should be equivalent up to a small translating constant to encoding a value $\epsilon$ near zero and sum to $\pi$. It seems not too hard to show that a "small" formula cannot produce a non-zero number that is too small. – Real Jun 13 '15 at 7:56
• @Real: You can just take a large integer $n$ (say made of $b$ bits) and then have the formula $\epsilon = (1/n) - (1/(n + 1)) = 1/(n(n + 1)$ which almost requires $2b$ bits for precise calculation. Thus I think it should be possible to have a small formula to generate a non-zero number that is too small. – Paramanand Singh Jun 13 '15 at 8:05
• @ParamanandSingh Actually, there must be some function of the size of a class of formulas that limits their output to some finite number greater than zero -- there are infinitely many almost-zero values to encode but only finitely many formulas up to a certain size. I'm afraid this bounding function is not computable for general formulas though, by reduction to the busy beaver problem (wherein the busy beaver would output many zeros and then a 1). – Real Jun 13 '15 at 8:08

(Too long for a comment.)

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

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

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

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

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.

• Great to have a slew of Bellard type formulas for $\pi$. +1 – Paramanand Singh Jun 21 '15 at 5:06