<s>[INST] Prove that $\int_0^\infty\left(\arctan \frac1x\right)^2 \mathrm d x = \pi\ln 2$ 
Prove $$\int_0^\infty\left(\arctan \frac1x\right)^2 \mathrm d x = \pi\ln 2$$

Out of boredom, I decided to play with some integrals and Inverse Symbolic Calculator and accidentally found this to my surprise
$$\int_0^\infty\Big(\arctan \frac1x\Big)^2 \mathrm d x = \pi\ln 2 \quad (\text{conjectural}) \,\,\, {\tag{1}} $$
Here is Wolfram Alpha computation which shows (1) to be true to 50 digits. Is (1) true and how to prove it?
I can calculate 
$$\int_0^\infty\arctan \frac{1}{x^2}\mathrm d x = \frac{\pi}{\sqrt2}$$
easily by expanding $\arctan$ into Maclaurin series. But how to proceed with $\arctan^2$?
 [/INST] Let
$$ I(a,b)=\int_0^\infty\left(\arctan \frac ax\right)\left(\arctan \frac bx\right) \mathrm d x. $$
Then
\begin{eqnarray}
\frac{\partial^2I(a,b)}{\partial a\partial b}&=&\int_0^\infty\frac{x^2}{(x^2+a^2)(x^2+b^2)}\mathrm d x\\
&=&\frac{1}{a^2-b^2}\int_0^\infty \bigg(\frac{a^2}{x^2+a^2}-\frac{b^2}{x^2+b^2}\bigg)\mathrm d x\\
&=&\frac{1}{a^2-b^2}\frac\pi2(a-b)\\
&=&\frac{\pi}{2}\frac{1}{a+b}
\end{eqnarray}
and hence
$$ I(1,1)=\frac{\pi}{2}\int_0^1\int_0^1\frac{1}{a+b}\mathrm d a\mathrm d b=\frac\pi2\int_0^1(\ln(b+1)-\ln b)\mathrm d b=\pi\ln2.$$
</s>