A product bound for two binary quadratic forms

Proved

WorkbookSource.base_30719

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

lean-workbooksource-checked

Let $a,b,c,d$ be reals . Show that $(a^2-ab+b^2)(c^2-cd+d^2) \geq \frac{2}{3}(a^2c^2-abcd+b^2d^2).

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

Preamble

import Mathlib
open Real Nat

Formal statement

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

Source