A cyclic four-variable quartic inequality

Proved

WorkbookSource.base_4009

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

lean-workbooksource-checked

Let $a,b,c,d$ are real numbers,prove that: $(b^2+c^2+d^2+a^2)^2\geq (c^2b+cd^2+a^2d+b^2a)(a+b+c+d).$

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

Preamble

import Mathlib
open Real Nat

Formal statement

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

Source