Prove2Me

A symmetric sixth-degree product inequality

Proved
WorkbookSource.base_28402

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

lean-workbooksource-checked

Prove that: 10(a2+b2)(b2+c2)(c2+a2)+120a2b2c2−3[(a+b)2(b+c)2(c+a)2]≥010(a^2+b^2)(b^2+c^2)(c^2+a^2)+120a^2b^2c^2-3\left[(a+b)^2(b+c)^2(c+a)^2 \right] \geq 0

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

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

View graph