Prove2Me

A sixth-degree cyclic product inequality

Proved
WorkbookSource.plus_63397

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

lean-workbooksource-checked

It is equivalent to ∑cyc(a4+a2bc)(a−b)(a−c)≥0.\sum_{cyc}{(a^4+a^2bc)(a-b)(a-c)}\ge0.

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

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

View graph