Prove2Me

lean_workbook_plus_62493

Disproved

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

Thus, it remains to prove that 7(x3+y3+z3)2≥(x5+y5+z5)(x+y+z)+2(x2y2+x2z2+y2z2)(x+y+z)27(x^3+y^3+z^3)^2\geq(x^5+y^5+z^5)(x+y+z)+2(x^2y^2+x^2z^2+y^2z^2)(x+y+z)^2 , which is ∑sym(3x6−x5y−2x4y2+5x3y3−4x3y2z−x2y2z2)≥0\sum_{sym}(3x^6-x^5y-2x^4y^2+5x^3y^3-4x^3y^2z-x^2y^2z^2)\geq0 , which is obvious.

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

View graph