Prove2Me

Nonnegativity of a sixth-degree difference polynomial

Proved
WorkbookSource.base_38173

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

lean-workbooksource-checked

The following inequality is equivalent to

4(a−b)2(−c+b)2(c−a)2+3∑b2c2(a−b)(a−c)+3abc∑a(a−b)(a−c)≥0 4(a-b)^2(-c+b)^2(c-a)^2+3\sum{b^2c^2(a-b)(a-c)}+3abc\sum{a(a-b)(a-c)}\geq 0

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_38173 (a b c : ℝ) : (4 * (a - b) ^ 2 * (-c + b) ^ 2 * (c - a) ^ 2 + 3 * (b ^ 2 * c ^ 2 * (a - b) * (a - c) + c ^ 2 * a ^ 2 * (b - a) * (b - c) + a ^ 2 * b ^ 2 * (c - a) * (c - b)) + 3 * a * b * c * (a * (a - b) * (a - c) + b * (b - a) * (b - c) + c * (c - a) * (c - b))) ≥ 0  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_38173; Apache-2.0

View graph