Prove2Me

lean_workbook_plus_46737

Proved

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

Prove that (a2+b2+c2)2≥(a(b2−bc+c2)+b(c2−ca+a2)+c(a2−ab+b2))(a+b+c) \left(a^{2}+b^{2}+c^{2}\right)^{2}\geq\left(a\left(b^{2}-bc+c^{2}\right)+b\left(c^{2}-ca+a^{2}\right)+c\left(a^{2}-ab+b^{2}\right)\right)\left(a+b+c\right)

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

View graph