lean_workbook_plus_10240

Proved

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

Show that $n=2$ in Schur's Inequality expands to $x^4+y^4+z^4+xyz(x+y+z)\ge x^3y+y^3z+z^3x+xy^3+yz^3+zx^3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_10240 (x y z : ℝ) : x ^ 4 + y ^ 4 + z ^ 4 + x * y * z * (x + y + z) ≥ x ^ 3 * y + y ^ 3 * z + z ^ 3 * x + x * y ^ 3 + y * z ^ 3 + z * x ^ 3   :=  by sorry

Source

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

View graph