lean_workbook_plus_25971

Proved

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

But then $x^2 - x - 1 = 0 \implies x = \frac{1 \pm \sqrt{5}}{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_25971  (x : ℝ)
  (h₀ : x^2 - x - 1 = 0) :
  x = (1 + Real.sqrt 5) / 2 ∨ x = (1 - Real.sqrt 5) / 2   :=  by sorry

Source