Recently I posted [a conjecture at Math.SE](https://math.stackexchange.com/questions/395818/closed-form-for-int-0-infty-ln-fracj-mux2y-mux2j-nux2y-nux):
$$\int\_0^\infty\ln\frac{J\_\mu(x)^2+Y\_\mu(x)^2}{J\_\nu(x)^2+Y\_\nu(x)^2}\mathrm dx\stackrel{?}{=}\frac{\pi}{2}(\mu^2-\nu^2),$$
where $J\_\mu(x)$ and $Y\_\mu(x)$ are the Bessel function of the [first](http://mathworld.wolfram.com/BesselFunctionoftheFirstKind.html) and [second](http://mathworld.wolfram.com/BesselFunctionoftheSecondKind.html) kind.
It is supported by numerical calculation with hundreds of digits of precision for many different values of $\mu, \nu$. The question is open for several days with +500 bounty on it and is not resolved yet. But my question here is not about if this conjecture true or false.


Obviously, several possible closed forms matched my numeric calculations, for example:
$$\left(\frac{\pi}{2}+7^{-7^{7^{7^{7^{7^{\sqrt{5}+\sin \mu\nu}}}}}}\right)(\mu^2-\nu^2).$$
But for some reason that I cannot clearly explain (or even understand) I selected the simpler one, and I am strongly inclined to search for its proof rather than a disproof. I believe most people would feel and behave exactly the same way. 



> 
> (1) Are there any mathematical or philosophical reasons supporting this position?
> 
> 
> 


Why when we calculate some sum or integral (which do not contain explicit tiny quantities like $10^{-10^{10^{.^{.^{10}}}}}$) with thousands of digits of precision and it matches some simple closed-form expression, we inclined to believe this is the exact equality rather than an accidental very close value? 



> 
> (2) Are there known cases when such intuition turned out to be wrong?
> 
> 
> 


And one more question:



> 
> (3) Do you believe there can be exact closed forms for some infinite sums or integrals, that cannot be proved in $ZFC$ or any its reasonable extension (like adding some large cardinal axioms) - so to speak, equalities that hold without any reason.
> 
> 
> 



How closed-form conjectures are made?
Part of what makes this question subtle is that what's intuitive depends on your background knowledge. In particular, the question of what counts as an "explicit tiny quantity" is hard to pin down. For example, Bailey, Borwein, and Borwein pointed out the example
$$
\left(\frac{1}{10^5} \sum\_{n=-\infty}^\infty e^{-n^2/10^{10}}\right)^2 \approx \pi,
$$
which holds to over 42 billion digits. If you know something about Poisson summation, it's pretty obvious that this is a fraud: Poisson summation converts this series into an incredibly rapidly converging series with first term $\pi$, after which everything else is tiny. Even if you don't know about Poisson summation, the $10^5$ and $10^{10}$ should raise some suspicions. However, it's a pretty amazing example if you haven't seen this sort of thing before.


As for the third question, the truth is more dramatic than that. There are *finite* identities that are independent of ZFC, or any reasonable axiom system, so you don't even need anything fancy like infinite sums or integrals. This follows from a theorem of Richardson (D. Richardson, *Some Undecidable Problems Involving Elementary Functions of a Real Variable*, Journal of Symbolic Logic **33** (1968), 514-520, <http://www.jstor.org/stable/2271358>).


Specifically, consider the expressions obtainable by addition, subtraction, multiplication, and composition from the initial functions $\log 2$, $\pi$, $e^x$, $\sin x$, and $|x|$. Richardson proved that there is no algorithm to decide whether such an expression defines the zero function. Now, if the function is not identically zero then it can be proved not to be zero (find a point at which it doesn't vanish and compute it numerically with enough accuracy to verify that it is nonzero). If all the identically zero cases could be proved in ZFC too, then that would give a decision procedure: do a brute force search through all possible proofs until you find one that resolves the question. Thus, there exists an expression that actually is identically zero but where there is no proof in ZFC. In fact, if you go through Richardson's proof you can explicitly construct such an expression, although it will be terrifically complicated. (To be precise, you'll be able to prove in ZFC that if ZFC is consistent, then this identity is unprovable, but by Gödel's second incompleteness theorem you won't be able to prove that ZFC is consistent in ZFC.)


Being independent of ZFC doesn't mean these identities are true for no reason, and in fact Richardson's proof gives a reason. However, his paper shows that there is no systematic way to test identities. You can indeed end up stuck in a situation where a proposed identity really looks true numerically but you just can't find a proof.


