Nonnegativity of a sum of cubes and a quadratic product

Proved

WorkbookSource.base_45570

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

If $a,b,c$ are real numbers, then

$(d)\ \ \ 2(a^2+bc)(b^2+ca)(c^2+ab)+a^6+b^6+c^6\ge 0.$

Source: InternLM Lean-Workbook, record lean_workbook_45570 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_45570 (a b c : ℝ) : 2 * (a ^ 2 + b * c) * (b ^ 2 + c * a) * (c ^ 2 + a * b) + a ^ 6 + b ^ 6 + c ^ 6 ≥ 0  :=  by sorry

Source