Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
All of them.... – abiessu Jan 8 '14 at 21:33
@abiessu How do you know that ? – mick Jan 8 '14 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 '14 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 '14 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 '14 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$)

share|cite|improve this answer
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 '14 at 23:03
Perhaps related : – mick Jan 8 '14 at 23:08
surley a loose upper bound can be computed. – nbubis Jan 8 '14 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}$$


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


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

share|cite|improve this answer
(+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 '14 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 '14 at 22:04
See my comment to MPW. – mick Jan 8 '14 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 '14 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 '14 at 22:38

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.