# How many digits do we need for a proof ??

In the question: Integral $\int_1^\infty\frac{\operatorname{arccot}\left(1+\frac{2\pi}{\operatorname{arcoth}x-\operatorname{arccsc}x}\right)}{\sqrt{x^2-1}}dx$, the value of that integral was conjectured to be $\frac{\pi\,\ln\pi}4-\frac{3\,\pi\,\ln2}8$.

Apart from the fact that this integral is interesting, I want to avoid this question to be a copy of that one, and my attention went to the statement:

the value is correct up to at least 900 decimal digits

My (imho) intuitive question is this: How many decimal digits are necessary to be considered a valid formal proof?

I know this is not the usual way to prove an integral, but since we have computers that can check many digits I think it is time to ask ourselves such questions !

I am aware of "mathematical coincidence," however I assume there must be limits to this coincidence.

I also understand that the amount of digits needed to be considered a proof depends on the "length" of the integrand and the conjectured value of the integral. By "length" I mean some measure of data size. For example the amount of functions, additions, multiplications, constants, etc. used.

-
All of them.... –  abiessu Jan 8 at 21:33
@abiessu How do you know that ? –  mick Jan 8 at 21:35
Because a formal proof means that it is fully proven that the result of the integral is $\frac{\pi\,\ln\pi}4-\frac{3\,\pi\,\ln2}8$, which means that every digit must be accounted for. It might be "accepted that the result is probably $\frac{\pi\,\ln\pi}4-\frac{3\,\pi\,\ln2}8$", but never fully proven unless every digit is verified, or the integral is proven to have that result directly. –  abiessu Jan 8 at 21:38
The idea is that after say 10^500 digits the result must be true ; not because it has been " explained " but because it cant be anything else ... –  mick Jan 8 at 21:57
Yes Jik , But thats exactly what the OP asks , a theory to compute $n$ or check $n$ or even prove the existance of $n$ or bound $n$ from above and below. –  mick Jan 8 at 22:21

The existence of such a criterion is clear: For a given "complexity" $L$ of mathematical expressions (given by the number of symbols etc.) there are only finitely many possible values. These form a discrete subset of $\mathbb R$ (or $\mathbb C$ or whatever - and ignoring any undefined expressions). Hence there exists an $\epsilon=\epsilon(L)>0$ such that two expressions that evaluate to values at most $\epsilon$ apart are in fact equal. However, it is more or less hopeless to explicitly determine such an $\epsilon$ for any interesting values of $L$ (e.g. big enough to allow both $\int_1^\infty\frac{\operatorname{arccot}\left(1+\frac{2\pi}{\operatorname{arcoth}x-\operatorname{arccsc}x}\right)}{\sqrt{x^2-1}}\,\mathrm dx$ and $\frac{\pi\ln\pi}4-\frac{3\pi\ln2}8$)

-
Thanks ! But are you saying it is not possible to compute $\epsilon$ ? And how to prove the statement that such $\epsilon$ exists ? –  mick Jan 8 at 23:03
Perhaps related : mathworld.wolfram.com/ConstantProblem.html –  mick Jan 8 at 23:08
surley a loose upper bound can be computed. –  nbubis Jan 8 at 23:09

Consider your question under the assumption that the value of the integral winds up being

$$\frac{\pi\,\ln\pi}4 \; -\; \frac{3\,\pi\,\ln2}8 \; + \; 10^{-901}$$

or

$$\frac{\pi\,\ln\pi}4 \; -\; \frac{3\,\pi\,\ln2}8 \; + \; 10^{-10000}$$

or

$$\frac{\pi\,\ln\pi}4 \; -\; \frac{3\,\pi\,\ln2}8 \; + \; 10^{-10^{100}}$$

-
(+1) - even though I can't really conceive of an integral having a true value of $\frac{\pi\,\ln\pi}4 \; -\; \frac{3\,\pi\,\ln2}8 \; + \; 10^{-10^{100}}$! –  Old John Jan 8 at 22:00
Nevertheless , that $10^{-1000}$ must come from somewhere. As I just wrote in the comment , Assume the output data size is a function of the imput data size. For instance it is unlikely that an integrand that contains only one exponential gives a final value that contains $10^{-10^{10^{10^{10}}}}$. –  mick Jan 8 at 22:04
See my comment to MPW. –  mick Jan 8 at 22:12
As an example : suppose I said the integral from 2 to + infinity of $\frac{dx}{\Gamma(x)}$ equals $3 + 100^{-100^{100^{100}}}$ then nobody would believe that ! And statistically that is almost impossible. –  mick Jan 8 at 22:26
@mick: Keep in mind that I could just as well have replaced the large negative powers of $10$ with comparably small numbers that are not rational, or even with numbers that are not expressible using standard mathematical constants and operations. –  Dave L. Renfro Jan 8 at 22:38