lean_workbook_plus_68474

Proved

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

Let $u = \sqrt[3]{2 + \sqrt{5}}$ and $v = \sqrt[3]{2 - \sqrt{5}}$ . Then $u^3 + v^3 = 4$ and $uv = -1$ . Now, let $x = u + v$ . Then $x^3 = u^3 + v^3 + 3uv(u + v) = 4 - 3x$ . Then $x^3 + 3x - 4 = 0$ . By the Rational Root Theorem/inspection, note that $x = 1$ works. Then $(x - 1)(x^2 + x + 4) = 0$ . Note that $x^2 + x + 4 = 0$ has no real roots, so $x = \boxed{1}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_68474  (u v x : ℝ)
  (h₀ : u = (2 + Real.sqrt 5)^(1 / 3))
  (h₁ : v = (2 - Real.sqrt 5)^(1 / 3))
  (h₂ : x = u + v)
  (h₃ : u^3 + v^3 = 4)
  (h₄ : u * v = -1) :
  x = 1   :=  by sorry

Source

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

View graph