An asymmetric four-variable quartic inequality

Proved

WorkbookSource.base_43118

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

lean-workbooksource-checked

Stronger:

$\\frac{1}{2} \\Bigl( 3(ad+bc-ac-bd)^2 + 3(ad-bc)^2 + (ac-bd)^2 \\Bigr) \\geq 0$

$\\iff 3a^2d^2 + 3b^2c^2 + 2a^2c^2 +2b^2d^2 + 2abcd \\geq 3a^2cd + 3d^2ab + 3c^2ab + 3b^2cd$

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

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_43118 {a b c d : ℝ} :
  3 * a ^ 2 * d ^ 2 + 3 * b ^ 2 * c ^ 2 + 2 * a ^ 2 * c ^ 2 + 2 * b ^ 2 * d ^ 2 + 2 * a * b * c * d ≥ 3 * a ^ 2 * c * d + 3 * d ^ 2 * a * b + 3 * c ^ 2 * a * b + 3 * b ^ 2 * c * d  :=  by sorry

Source

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

View graph