Prove2Me

lean_workbook_plus_27990

Proved

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

a,b,c are real numbers such that a+b+c=0a+b+c=0\nprove that:\n\n (a2+b2+c2)3≥27a2b2c2+(a−b)2(b−c)2(c−a)2(a^2+b^2+c^2)^3 \geq 27a^2b^2c^2+ (a-b)^2(b-c)^2(c-a)^2

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

View graph