Prove2Me

A weighted sixth-degree Schur-type inequality

Proved
WorkbookSource.plus_72831

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

lean-workbooksource-checked

Prove that (a3b+a3c)(a−b)(a−c)+(b3a+b3c)(b−a)(b−c)+(c3a+c3b)(c−a)(c−b)≥0(a^3b+a^3c)(a-b)(a-c)+(b^3a+b^3c)(b-a)(b-c)+(c^3a+c^3b)(c-a)(c-b) \geq 0 where a,b,c≥0a, b, c \geq 0.

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.plus_72831 (a b c : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) : (a^3 * b + a^3 * c) * (a - b) * (a - c) + (b^3 * a + b^3 * c) * (b - a) * (b - c) + (c^3 * a + c^3 * 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_72831; Apache-2.0

View graph