lean_workbook_plus_5244

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

After using Cauchy Schwarts, it's becomes: \n $\sum\ (a - b)^2(b - c)^2 + 3(abc - 1)^2 + 3 - abc \geq\ 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_5244 (a b c : ℝ) : (a - b) ^ 2 * (b - c) ^ 2 + 3 * (a * b * c - 1) ^ 2 + 3 - a * b * c ≥ 0   :=  by sorry

Source