Two solutions of a conjugate cube-root equation

Proved

WorkbookCorrected.plus_51554

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

corrected-formalizationlean-workbooksource-checked

For real $x$ ,

\sqrt[3]{20+x\sqrt2}+\sqrt[3]{20-x\sqrt2}=4

holds if and only if $x=14$ or $x=-14$ .

Formalization Note: Real cube roots are specified by their cubing equations. This corrects the natural-number division used in the original fractional powers and includes both directions of the source solution classification.

Source: InternLM Lean-Workbook, record lean_workbook_plus_51554 (Apache-2.0).

Preamble

import Mathlib

Formal statement

theorem WorkbookCorrected.plus_51554 : ∀ (x : ℝ),
    (∃ a b : ℝ, a^3=20+x*Real.sqrt 2 ∧ b^3=20-x*Real.sqrt 2 ∧ a+b=4) ↔
    (x=14 ∨ x= -14) := by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_51554; Apache-2.0

View graph