Prove2Me

lean_workbook_plus_72124

Proved

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

Let x,y,z≥0,x(y+z)(x+y+z)=1x,y,z \geq 0, x(y+z)(x+y+z)=1, prove that: (x+y+z)3≥4(x+y+z)^3 \geq 4.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_72124 (x y z : ℝ) (hx : x ≥ 0) (hy : y ≥ 0) (hz : z ≥ 0) (h : x * (y + z) * (x + y + z) = 1) : (x + y + z) ^ 3 ≥ 4   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph