lean_workbook_plus_41249

Proved

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

Either, note that\n $\left(a^4+b^4+c^4\right)+3\left(b^2c^2+c^2a^2+a^2b^2\right)$ \n $-2\left(bc\left(b^2+c^2\right)+ca\left(c^2+a^2\right)+ab\left(a^2+b^2\right)\right)$ \n $=\left(\frac{b^4+c^4}{2}+3b^2c^2-2bc\left(b^2+c^2\right)\right)+\left(\frac{c^4+a^4}{2}+3c^2a^2-2ca\left(c^2+a^2\right)\right)$ \n $+\left(\frac{a^4+b^4}{2}+3a^2b^2-2ab\left(a^2+b^2\right)\right)$ \n $=\frac{\left(b-c\right)^4}{2}+\frac{\left(c-a\right)^4}{2}+\frac{\left(a-b\right)^4}{2}\geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_41249 {a b c : ℝ} :
  a^4 + b^4 + c^4 + 3 * (b^2 * c^2 + c^2 * a^2 + a^2 * b^2) -
    2 * (b * c * (b^2 + c^2) + c * a * (c^2 + a^2) + a * b * (a^2 + b^2)) ≥ 0   :=  by sorry

Source

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

View graph