Prove2Me

A sixth-degree bound involving pairwise power differences

Proved
WorkbookSource.plus_55022

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

lean-workbooksource-checked

Let a,b,c>0a,b,c > 0 . Prove that : (a5−b5)(a−b)+(b5−c5)(b−c)+(c5−a5)(c−a)≥5ab(a2+b2−ac−bc)(a−b)2+5bc(b2+c2−ba−ca)(b−c)2+5ca(c2+a2−cb−ab)(c−a)2(a^5 - b^5 )(a-b)+(b^5 - c^5 )(b-c) + (c^5 -a^5 )(c-a) \geq 5ab(a^2 +b^2 -ac-bc)(a-b)^2 + 5bc(b^2 +c^2 -ba-ca )(b-c)^2 + 5ca(c^2 +a^2 -cb-ab )(c-a)^2

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

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

View graph