Prove2Me

lean_workbook_plus_5906

Disproved

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

Prove that ab(a−b)2+2(ab−1)(a2+b2)+4(ab−2)(a+b−2)≥0ab(a-b)^{2}+2(ab-1)(a^{2}+b^{2})+4(ab-2)(a+b-2)\geq 0

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5906 : ∀ a b : ℝ, a * b * (a - b) ^ 2 + 2 * (a * b - 1) * (a ^ 2 + b ^ 2) + 4 * (a * b - 2) * (a + b - 2) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph