Prove2Me

lean_workbook_plus_9491

Proved

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

If a, b, c are real number then: (a2+b2+c2)2−2abc(a+b+c)≥2(a+b+c)(a−b)(b−c)(a−c)(a^2+b^2+c^2)^2-2abc(a+b+c)\ge 2(a+b+c)(a-b)(b-c)(a-c)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_9491 (a b c : ℝ) : (a^2 + b^2 + c^2)^2 - 2 * a * b * c * (a + b + c) ≥ 2 * (a + b + c) * (a - b) * (b - c) * (a - c)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph