Bounds on a sum under a cube-root constraint

Proved

WorkbookCorrected.plus_18160

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

corrected-formalizationlean-workbooksource-checked

Let $a,b\ge0$ satisfy $\sqrt[3]{1+a}+\sqrt[3]{1+2b}=3$ . Then

\frac{159}{2}-54\sqrt2\le a+b\le7.

Formalization Note: Real cube roots are expressed through their cubing equations. This repairs the natural-number division in the original fractional exponents and preserves the nonnegative domain, root-sum condition and both requested bounds.

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

Preamble

import Mathlib

Formal statement

theorem WorkbookCorrected.plus_18160 : ∀ (a b u v : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hu : u^3=1+a) (hv : v^3=1+2*b) (h : u+v=3),
    159/2-54*Real.sqrt 2 ≤ a+b ∧ a+b ≤ 7 := by sorry

Source

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

View graph