A squared cyclic quadratic expression bounds a cubic product

Proved

WorkbookSource.base_33177

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

lean-workbooksource-checked

a,b,c,d $\in$ R ,prove that:

$\left( {a}^{2}+ab+{b}^{2}+bc+{c}^{2}+cd+{d}^{2}+ad \right) ^{2}\geq 2\, \left( a+b+c+d \right) \left( ab \left( a+b \right) +cb \left( b+c \right) +dc \left( c+d \right) +ad \left( d+a \right) \right)$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_33177 (a b c d : ℝ) : (a^2 + a * b + b^2 + b * c + c^2 + c * d + d^2 + d * a)^2 ≥ 2 * (a + b + c + d) * (a * b * (a + b) + b * c * (b + c) + c * d * (c + d) + d * a * (d + a))  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_33177; Apache-2.0

View graph