Prove2Me

lean_workbook_plus_61558

Disproved

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

x5+y5+z5≥3(x3+y3+z3−x2−y2−z2)+x2+y2+z2≥x2+y2+z2x^5+y^5+z^5\ge3(x^3+y^3+z^3-x^2-y^2-z^2)+x^2+y^2+z^2 \ge x^2+y^2+z^2

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

View graph