lean_workbook_plus_3188

Proved

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

substitution $x_1 = \mu x,x_2 = \mu y,x_3 = \mu z,x_4 = \mu w$ from $x_1^3 + x_2^3 + x_3^3 + x_4^3 = 4$ we have $\mu^3 = \frac {4}{x^3 + y^3 + z^3 + w^3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3188    (x y z w : ℝ)
    (h : x^3 + y^3 + z^3 + w^3 = 4) :
    ∃ μ : ℝ, μ^3 = 4 / (x^3 + y^3 + z^3 + w^3)   :=  by sorry

Source

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

View graph