Prove2Me

A product of two quartic differences bounds a squared cyclic expression

Proved
WorkbookSource.base_36463

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

lean-workbooksource-checked

Prove that: (∑cyca2b2−abc(a+b+c))(∑cyca4−∑cyca2b2)≥34(∑cyca3b−abc(a+b+c))2 \left(\sum_{cyc}a^2b^2 - abc(a + b + c)\right)\left(\sum_{cyc}a^4 - \sum_{cyc}a^2b^2\right) \ge \frac {3}{4}\left(\sum_{cyc}a^3b - abc(a + b + c)\right)^2

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

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

View graph