lean_workbook_plus_42648

Proved

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

Let $x = \dfrac{1 + \sqrt{5}}{2}$ . Thus $2x - 1 = \sqrt{5}$ . Squaring, $4x^2 - 4x + 1 = 5$ , or $4x^2 - 4x - 4 = 0$ , or $\boxed{x^2 - x - 1 = 0}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph