lean_workbook_plus_39031

Proved

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

Prove that $4x+y^3z+yz^3 \ge 6 \sqrt[6] {x^4y^4z^4}=6$ given $x,y,z>0$ and $xyz=1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39031 (x y z : ℝ) (hx : x>0) (hy : y>0) (hz : z>0) (habc : x*y*z = 1) : 4*x + y^3*z + y*z^3 >= 6 * (x^4*y^4*z^4)^(1/6)   :=  by sorry

Source

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

View graph