lean_workbook_plus_13758

Proved

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

According to Albania Eagle, we have: $3(x^4+y^4+z^4)+3xyz(x+y+z) \geq 2 (xy+yz+xz)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

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

Source

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

View graph