lean_workbook_plus_20076

Proved

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

Let $a=b+x$ and $d=c+y$ . Ineq becomes\n\n $6(x^2+y^2)+(x+y)^2+4(x+y)(b+c)+4(b+c)^2-12bc \ge 0$ ,\n\n $3(x-y)^2+3(b-c)^2+(2x+2y+b+c)^2 \ge 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20076 {a b c d x y : ℝ} (hab : a = b + x) (hcd : d = c + y) :
  6 * (x ^ 2 + y ^ 2) + (x + y) ^ 2 + 4 * (x + y) * (b + c) + 4 * (b + c) ^ 2 - 12 * b * c ≥ 0 ∧
  3 * (x - y) ^ 2 + 3 * (b - c) ^ 2 + (2 * x + 2 * y + b + c) ^ 2 ≥ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph