lean_workbook_plus_2737

Disproved

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

Prove that $x^{4}+y^{4}+z^{4}+(x^{2}+y^{2}+z^{2})(xy+yz+zx) \ge 4(x^{2}y^{2}+y^{2}z^{2}+z^{2}x^{2})$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2737 : ∀ x y z : ℝ, x ^ 4 + y ^ 4 + z ^ 4 + (x ^ 2 + y ^ 2 + z ^ 2) * (x * y + y * z + z * x) ≥ 4 * (x ^ 2 * y ^ 2 + y ^ 2 * z ^ 2 + z ^ 2 * x ^ 2)   :=  by sorry

Source

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

View graph