A012: ∫₀¹ arctan x / (x+1) · log x dx = -π³/64 + (G/2) log 2 #
Integrate by parts with u = arctan x and v = Li₂(-x) + log x · log(1+x), an antiderivative of
log x/(1+x) that is continuous on [0, 1] (Lean's log 0 = 0 gives v(0) = 0). The boundary
term is (π/4) Li₂(-1) = -π³/48, so the integral equals
-π³/48 - ∫₀¹ Li₂(-x)/(1+x²) dx - M, where M = ∫₀¹ log x · log(1+x)/(1+x²) dx.
Writing Li₂(-x) = ∫₀¹ x log y/(1+xy) dy and swapping the order of integration turns
∫₀¹ Li₂(-x)/(1+x²) dx into ∫₀¹ log y · K(y) dy with the kernel
K(y) = (log 2/2 + πy/4 - log(1+y))/(1+y²). The log(1+y) part of the kernel gives -M, which
cancels, and what is left is (log 2/2) ∫₀¹ log y/(1+y²) dy + (π/4) ∫₀¹ y log y/(1+y²) dy
= -(G/2) log 2 - π³/192.