lean_workbook_plus_53382

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

So the fraction is $\left(\frac{\sqrt{5}-1}{\sqrt{5}+1}\right)^2$ , which is equivalent to $\frac{7-3\sqrt{5}}{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53382 (x : ℝ) : ((Real.sqrt 5 - 1) / (Real.sqrt 5 + 1))^2 = (7 - 3 * Real.sqrt 5) / 2   :=  by sorry

Source