A003: Li₂((√5-1)/2) = π²/10 - log²((1+√5)/2)

Let x = (√5 - 1)/2 = 1/φ, where φ = (1 + √5)/2. Then x² = 1 - x and 1 + x = 1/x = φ. Three dilogarithm identities at x give a linear system for Li₂(x), Li₂(x²) and Li₂(-x):

• Euler's reflection formula, with 1 - x = x²: Li₂(x) + Li₂(x²) = π²/6 - 2 log² x;
• the duplication formula: Li₂(x²) = 2 Li₂(x) + 2 Li₂(-x);
• Landen's identity, with x/(1+x) = x²: Li₂(-x) + Li₂(x²) = -½ log² x.

Solving it gives Li₂(x) = π²/10 - log² x, and log² x = log² φ because x = 1/φ.

theorem LeanPolyLog.Proofs.A003 : Lir 2 ((√5 - 1) / 2) = Real.pi ^ 2 / 10 - Real.log ((1 + √5) / 2) ^ 2

A003: Li₂((√5-1)/2) = π²/10 - log²((1+√5)/2).