Prove2Me

lean_workbook_plus_35946

Proved

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

For #1 \nIndeed，the inequality is also true for any real numbers a,ba,b and cc . \nBecause of (a2+b2+c2)3−3(a2b+b2c+c2a)2=2∑a2c2(a−b)2+∑(ab2−c3)2≥0(a^2+b^2+c^2)^3-3(a^2b+b^2c+c^2a)^2=2\sum{a^2c^2(a-b)^2}+\sum{(ab^2-c^3)^2}\ge{0}

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

View graph