Prove2Me

lean_workbook_plus_65368

Disproved

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

For the second inequality Setting a=x2,b=y2,c=z2a=x^2,b=y^2,c=z^2 It is equivalent to ∑x4+∑symx3y+∑x2yz≥4∑x2y2\sum{x^4}+\sum_{sym}{x^3y} +\sum{x^2yz} \geq 4\sum{x^2y^2} ⇔\Leftrightarrow ∑cyc(x4+2x3y−6x2y2+2xy3+y4)+∑cyc(−x2y2+2x2yz−x2z2)≥0\sum_{cyc}{(x^4+2x^3y-6x^2y^2+2xy^3+y^4)} +\sum_{cyc}{(-x^2y^2+2x^2yz-x^2z^2)} \geq 0 ⇔\Leftrightarrow ∑cyc(x−y)2(x2+4xy+y2−z2)≥0\sum_{cyc}{(x-y)^2(x^2+4xy+y^2-z^2)} \geq 0

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

View graph