A005: ∫₀¹ log²(1+x²)/x³ dx = π²/12 - log²2

Write L(x) = log(1+x²) and H(x) = -L(x)²/(2x²) - L(x)²/2. For x ≠ 0, H'(x) = L(x)²/x³ - 2 L(x)/x, so ∫₀¹ L²/x³ = (H(1) - H(0)) + 2 ∫₀¹ L/x = -log²2 + 2 · π²/24 by the fundamental theorem of calculus and A004.

In Lean H 0 = 0 and the integrands take the value 0 at x = 0. All three functions are continuous at 0, because 0 ≤ L(x) ≤ x².

theorem LeanPolyLog.Proofs.A005 : ∫ (x : ℝ) in 0..1, Real.log (1 + x ^ 2) ^ 2 / x ^ 3 = Real.pi ^ 2 / 12 - Real.log 2 ^ 2

A005: ∫₀¹ log²(1+x²)/x³ dx = π²/12 - log²2.