Today @integralsbot at twitter posted an interesting integral relation for complicated integral that gives $\pi$ as a result. I don't know how this bot works or where does it take the relation it posts from, but some of the problems are really difficult to prove and interesting. Such as this example.
$$\int_{0}^{\infty} \frac{\left(\frac{\pi x}{2}-\log (x)\right)^3}{\left(x^2+1\right)^2 \left(\log^2(x)+\frac{\pi ^2}{4}\right)} = \pi \tag{1}\label{eq1}$$
I've tried to calculate this and it appears to be very difficult (for starters wolfram alpha can't calculate it). The plot of the function under the integral doesn't look very extraordinarily:
Using partial fraction decomposition the integral can be transformed to the following form:
$$\int_{0}^{\infty} \left( \frac{3 \pi x}{2 \left(x^2+1\right)^2}-\frac{\log (x)}{\left(x^2+1\right)^2}+\frac{\pi^3 x^3-6 \pi ^2 x^2 \log (x)-3 \pi ^3 x+2 \pi ^2 \log (x)}{2 \left(x^2+1\right)^2 \left(4\log ^2(x)+\pi ^2\right)} \right)$$
The first two terms of the integral can be more $$ \int_{0}^{\infty} \frac{3 \pi x}{2 \left(x^2+1\right)^2} = \frac{3 \pi}{4} $$ or less easily solved $$ \int_{0}^{\infty} -\frac{\log (x)}{\left(x^2+1\right)^2} = \frac{\pi}{4} $$ to yield: $$ \int_{0}^{\infty} \left( \frac{3 \pi x}{2 \left(x^2+1\right)^2} - \frac{\log (x)}{\left(x^2+1\right)^2} \right) = \pi \tag{2}\label{eq2} .$$
This is interesting by itself, since plot of the integrated function has interesting shape with two inflection points of the first derivative, which I wouldn't expect to be equal to $\pi$ (of course the algebra clearly shows that it is)
What's however even more interesting is that, if I'm not mistaken, it follows from \eqref{eq1} and \eqref{eq2} that
$$ \int_{0}^{\infty} \frac{\pi^3 x^3-6 \pi ^2 x^2 \log (x)-3 \pi ^3 x+2 \pi ^2 \log (x)}{2 \left(x^2+1\right)^2 \left(4\log ^2(x)+\pi ^2\right)} = 0 \tag{3}\label{eq3}.$$
This seems to be correct when checked with numerical integration (I've checked in relatively high precision of ~100 decimal digits) but seem to be very hard to prove. Plot of the function under the integral \eqref{eq3} doesn't appear (to me) to suggest any trivial solution:
The most obvious way to transform integral \eqref{eq3} is to expand the numerator which gives:
$$ \int_{0}^{\infty} \left( -\frac{3 \pi ^2 x^2 \log (x)}{\left(x^2+1\right)^2 \left(4 \log ^2(x)+\pi ^2\right)}-\frac{3 \pi ^3 x}{2 \left(x^2+1\right)^2 \left(4 \log ^2(x)+\pi ^2\right)}+\frac{\pi ^2 \log (x)}{\left(x^2+1\right)^2 \left(4 \log ^2(x)+\pi ^2\right)}+\frac{\pi ^3 x^3}{2 \left(x^2+1\right)^2 \left(4 \log ^2(x)+\pi ^2\right)} \right), $$
but the resulting integrals are also very difficult, perhaps too difficult to directly attack the problem in this way (I've tried to solve the second one, since it seems to have the simplest numerator, but didn't managed to get any results yet) and neither their numerical values (-1.93789..., 3.229820..., -0.322982..., -0.968946...) nor the plots indicate any obvious cancellations. Maybe there is some indirect way? Perhaps the integral \eqref{eq3} can be shown to be equal to $0$ without directly solving the integral at all?
As I mentioned in the beginning of this post, I don't know where does this \eqref{eq1} relation come from but it seems to be true and interesting and must've been found somehow. Therefore I believe some solution of this problem exists. I post it as an interesting challenge/puzzle. Maybe someone knows some of the relations, can solve some of the unsolved integrals, sees clever substitution or can provide any interesting insight into this problem. So, to finally pose the question.
How to prove/solve either \eqref{eq1} or \eqref{eq3}?