Prove2Me

A cyclic quartic inequality at fixed total three

Proved
WorkbookSource.plus_40795

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

lean-workbooksource-checked

Given a+b+c=3a+b+c=3, prove that 6∑a4−4∑a3c−37∑a3b+91∑a2b2−56∑a2bc≥06\sum{a^{4}}-4\sum{a^{3}c}-37\sum{a^{3}b}+91\sum{a^{2}b^{2}}-56\sum{a^{2}bc}\geq 0

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

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

View graph