Prove2Me

lean_workbook_plus_52971

Proved

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

Prove that for real numbers a,b,ca, b, c such that a+b+c=0a + b + c = 0, the following inequality holds: (a2+b2+c2)3≥2(a−b)2(b−c)2(c−a)2(a^2 + b^2 + c^2)^3 \geq 2(a - b)^2(b - c)^2(c - a)^2.

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

View graph