Prove2Me

lean_workbook_plus_24414

Proved

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

Prove that (x3+y3+z3)2+4(xyz)2≥2(y3z3+z3x3+x3y3)(x^3+y^3+z^3)^2 + 4 \Big( xyz \Big ) ^2 \geq 2 \Big( y^3z^3+z^3x^3+x^3y^3 \Big) for x,y,z∈Rx,y,z \in R.

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

View graph