A four-variable cyclic quartic expression is nonnegative

Proved

WorkbookSource.base_15265

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

lean-workbooksource-checked

prove that: $(a^2-2ab+c^2)(a^2+bc)+(b^2-2bc+d^2)(b^2+cd)+(c^2-2cd+a^2)(c^2+ad)+(-2ad+d^2+b^2)(d^2+ab)\geq 0$

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

Preamble

import Mathlib
open Real Nat

Formal statement

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

Source

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

View graph