Prove2Me

lean_workbook_plus_8392

Proved

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

Let x,y,z∈Rx,y,z \in R ,prove that: (x3y+zy3+xz3)(xy+yz+xz)≥(x+y+z)xyz(x2+y2+z2).(x^3y+zy^3+xz^3)(xy+yz+xz) \geq (x+y+z)xyz(x^2+y^2+z^2).

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

View graph