A hard integral identity on MathSE

$$\int_0^{1}\arctan\left(\frac{\mathrm{arctanh}\ x-\arctan{x}}{\pi+\mathrm{arctanh}\ x-\arctan{x}}\right)\frac{dx}{x}=\frac{\pi}{8}\log\frac{\pi^2}{8}$$

seems to be very difficult to prove.

Question: I worked on this identity for several days without any success. Is there any clue how to prove this integral identity?

• I'm waiting for Noam Elkies's solution :-) Jan 18, 2014 at 19:20
• A related problem can be found here. Jan 21, 2014 at 15:08
• What happens if $\pi$ in the integral is replaced by some other real number? Can one give a closed-form formula for the integral in this case? Jan 23, 2014 at 5:32
• Where does this problem come from and why do you care about it? Jan 24, 2014 at 3:46
• @LevBorisov: This identity is a long-lasting problem(which was raised by another user) on Math.SE, and I think it is just the type of identity which may appear in Ramanujan's notebooks. Although I don't know what this identity may related to, it would be better to draw more attention to this elegent identity. Jan 28, 2014 at 12:15

The function $$G(z)=\frac{\log(1+(1+i)\,f(z)\,)}z$$ where $$f(x)=\frac{\operatorname{arctanh}(x)-\arctan(x)}{\pi}$$ extended analytically.
• That's great. I suggest that you at least copy the definitions of the key functions $f(z)$ and $G(z)$ into your answer. Feb 18, 2014 at 8:57