lean_workbook_plus_45324

Proved

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

We have to prove that: $(a^2+b^2+c^2)^2 \geq (a+b+c)[ab(a+b)+bc(b+c)+ca(c+a)-3abc]$ $\Leftrightarrow$ $a^4+b^4+c^4+abc(a+b+c) \geq bc(b^2+c^2) + ca(c^2+a^2) + ab(a^2+b^2)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45324 (a b c: ℝ) : (a^2+b^2+c^2)^2 ≥ (a+b+c)*(a*b*(a+b) + b*c*(b+c) + c*a*(c+a) - 3*a*b*c) ↔ a^4+b^4+c^4+(a*b*c)*(a+b+c) ≥ b*c*(b^2+c^2) + c*a*(c^2+a^2) + a*b*(a^2+b^2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph