Prove2Me

A sixth-degree inequality formed from pairwise differences

Proved
WorkbookSource.plus_2894

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

lean-workbooksource-checked

This inequality holds for all reals a,b,ca,b,c

4∑(a−b)(a−c)(a2−b2)(a2−c2)+(a−b)2(b−c)2(c−a)2≥0.4\sum (a-b)(a-c)(a^2-b^2)(a^2-c^2)+(a-b)^2(b-c)^2(c-a)^2\ge 0.

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

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

View graph