How many digits do we need for a proof ??

Question

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}}\mathrm 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.

Answer 1

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}}$$

Answer 2

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$)