A symmetric quartic expression is nonnegative
ProvedWorkbookSource.base_11191lean-workbooksource-checked
(a^{2}+b^{2})(a-b)^{2}+(b^{2}+c^{2})(b-c)^{2}+(c^{2}+a^{2})(c-a)^{2}+2abc(a+b+c) \ge 0$
Source: InternLM Lean-Workbook, record lean_workbook_11191 (Apache-2.0). Complete source proposition preserved; proof developed independently.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.base_11191 (a b c : ℝ) : (a^2 + b^2) * (a - b)^2 + (b^2 + c^2) * (b - c)^2 + (c^2 + a^2) * (c - a)^2 + 2 * a * b * c * (a + b + c) ≥ 0 := by sorry
Source