lean_workbook_plus_64657

Proved

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

First equation is $(x-\\sqrt 3)^3=64$ and so, assuming we are speaking of real numbers, $x=4+\\sqrt 3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64657 (x : ℝ) (hx : (x - Real.sqrt 3)^3 = 64) : x = 4 + Real.sqrt 3   :=  by sorry

Source