Prove2Me

A quartic inequality involving an antisymmetric product

Proved
WorkbookSource.base_30439

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

lean-workbooksource-checked

If a, b, c are real number then: (a2+b2+c2)2−3abc(a+b+c)≥3(a+b+c)(a−b)(b−c)(c−a)(a^2+b^2+c^2)^2-3abc(a+b+c) \ge 3(a+b+c)(a-b)(b-c)(c-a)

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

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

View graph