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$?
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)$.