Experimental mathematics: how are floating point equations discovered/converted to exact equations?

Question

the 2005 AMS article/survey on experimental mathematics[1] by Bailey/Borwein mentions many remarkable successes in the field including new formulas for $\pi$ that were discovered via the PSLQ algorithm as well as many other examples. however, it appears to glaringly leave out any description of the crucial step. it goes from discussing large accuracy floating point operations/formulas to stating the exact theoretical formulas with no discussion of the intermediate step(s).

suppose a floating point formula is found experimentally that holds for many finite points of the formula to a high degree of precision. how is it proven that the abstract algebraic formula which does not use floating point arithmetic with finite accuracy is correct?

this seems to relate to induction. of course a formula can hold for a finite number of points or finite precision but then fail for more points or "infinite" precision. is there any discussion that focuses on this step/conversion/aspect? of course a virtually identical/analogous issue arises in statistics with curve fitting and the danger of "overfitting".

[1] Experimental Mathematics: Examples, Methods and Implications by Bailey/Borwein, notes of the AMS, 2005

Answer 1

In most situations, floating point approximations can not prove a closed-form formula. An exception: if the value of an expression is known to be a member of a given discrete set, an accurate enough approximation can discriminate between members of that set. But once discovered by numerical methods, the BBP formula and similar ones are proven by standard techniques. In the BBP case, note that $$ \sum_{k=0}^\infty \frac{z^{8k+j}}{8k+j} = \int_0^z \sum_{k=0}^\infty t^{8k+j-1}\ dt = \int_0^z \frac{t^{j-1}}{1-t^8}\ dt$$ which can be evaluated using partial fractions, and the results combined and simplified to obtain $\pi$.