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$?
 A: Note that $\arctan \frac{1}{x} = \frac{\pi}{2} - \arctan x$ (simply draw a triangle with side $1$ and $x$ and consider the two angles). We then obtain $$I = \int_0^\infty \left( \arctan \frac{1}{x} \right)^2 \mathrm d x = \int_0^\infty \left( \frac{\pi}{2} - \arctan x \right)^2 \mathrm d x,$$
and we make the substitution $x = \tan u$ to obtain $$I = \int_0^{\frac{\pi}{2}} \sec^2 u \left( \frac{\pi}{2} - u \right)^2 \mathrm d u = \int_0^{\frac{\pi}{2}} \sec^2 u \left( \frac{\pi}{2} - u \right)^2 \mathrm d u$$ and again making a substitution $v = \frac{\pi}{2} - u$ gives
$$\int_0^{\frac{\pi}{2}} \frac{v^2}{\sin^2(v)} \mathrm d v$$
which is in fact evaluatable (although requires the polylogarithm function to express):
$$\int \frac{v^2}{\sin^2(v)} \mathrm d v = -i(v^2 + \mathrm{Li}_2(e^{2iv}))-v^2 \cot(v) + 2v \ln(1-2e^{iv}) + c,$$ upon which evaluating at both bounds gives $\pi \ln (2)$.
A: Take $x=\cot t$, the required integral becomes $$I=\int t^2 \csc^2 t~ dt= -t^2 \cot t-\int 2 t \cot t~ dt= -t^2 \cot t-2t \ln \sin t+ \int  2 \ln \sin t ~ dt. $$ Taking limits from $t=\pi/2$ to $x=0$ and using the well known integral $$\int_{0}^{\pi/2} \ln \sin t ~dt=-\frac{\pi}{2} \ln 2,$$ we get the required result.
A: Letting $y=\arctan \frac{1}{x} $ yields
$$
\begin{aligned}
I=& \int_0^{\frac{\pi}{2}} y^2 \csc ^2 y d y \\
&=-\int_0^{\frac{\pi}{2}} y^2 d(\cot y) \\
&=-\left[y^2 \cot y\right]_0^{\frac{\pi}{2}}+2 \int_0^{\frac{\pi}{2} } y \cot yd y \\
&=2 \int_0^{\frac{\pi}{2}} y d(\ln (\sin y))\\&= 2[y \ln (\sin y)]_0^{\frac{\pi}{2}}-2 \int_0^{\frac{\pi}{2}} \ln (\sin y) d y\\&=\pi \ln 2
\end{aligned}
$$
A: $$\int_0^\infty \arctan^2\left(\frac{1}{x}\right)dx\overset{\frac{1}{x}\to t}=\int_0^\infty \frac{\arctan^2 t}{t^2}dt\overset{IBP}=2\int_0^\infty \frac{\arctan t}{t(1+t^2)}dt$$
$$\overset{t=\tan x}=2\int_0^\frac{\pi}{2} \frac{x}{\tan x}dx\overset{IBP}=-2\int_0^\frac{\pi}{2}\ln(\sin x)dx=\pi\ln 2$$
See here for the last integral.
A: First the substitution $x\mapsto 1/x$ and then integration by parts yield
$$\int_0^\infty\arctan^2x^{-1}\,dx=2\int_0^\infty\frac{\arctan x}{x(1+x^2)}\,dx$$
so it suffices to evaluate the integral on the right. Define the function
$$f(a)=\int_0^\infty\frac{\arctan (ax)}{x(1+x^2)}\,dx$$
and differenciate with respecto to $a$ to obtain
$$f'(a)=\int_0^\infty\frac{dx}{(1+x^2)(a^2+x^2)}=
\frac\pi2\frac1{1+a}.$$
Thus
$$f(a)=\frac\pi2\log(1+a)+C$$
where the constant $C$ can be seen to be $0$ letting $a=0$. The result is now immediate letting $a=1$. 
A: 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.$$
A: As others have mentioned, you may use the fact that $\arctan(x)+\arctan\left(\frac1x\right)=\frac\pi2$ when $x>0$. We can also "fold up" the integral at $x=1$ to write
$$\begin{align*}
I &= \int_0^\infty \arctan^2\left(\frac1x\right) \, dx \\[1ex]
&= \left\{\int_0^1 + \int_1^\infty\right\} \left(\frac\pi2 - \arctan(x)\right)^2 \, dx \\[1ex]
&= \int_0^1 \left(\frac\pi2 - \arctan(x)\right)^2 \, dx + \int_0^1 \left(\frac\pi2 - \arctan\left(\frac1x\right)\right)^2 \, \frac{dx}{x^2} \\[1ex]
&= \int_0^1 \left(\frac{\pi^2}4 - \pi \arctan(x) + \arctan^2(x) + \frac{\arctan^2(x)}{x^2}\right) \, dx \\[1ex]
&= \frac\pi2 \log(2) + \int_0^1 \left(1+\frac1{x^2}\right) \arctan^2(x) \, dx
\end{align*}$$
and from (1) and (2) we find the remaining integral to make up the difference so $I=\pi\log(2)$.
