lean_workbook_plus_1162

Proved

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

$\Rightarrow 28\left( {x^4 + y^4 + z^4 } \right) \geqslant \left( {x + y + z} \right)^4 + \left( {y + z - x}\right)^4 + \left( {z + x - y} \right)^4 + \left( {x + y - z} \right)^4$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1162 : ∀ x y z : ℝ, 28 * (x ^ 4 + y ^ 4 + z ^ 4) ≥ (x + y + z) ^ 4 + (y + z - x) ^ 4 + (z + x - y) ^ 4 + (x + y - z) ^ 4   :=  by sorry

Source

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

View graph