Prove2Me

lean_workbook_plus_4390

Disproved

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

Yes, and I think next, we have LHS≥a2+b2+(3−a−b)2+3/2ab(3−a−b)−9/2LHS \ge {a^2} + {b^2} + {\left( {3 - a - b} \right)^2} + 3/2ab\left( {3 - a - b} \right) - 9/2 \nWe just need to prove a2+b2+(3−a−b)2+3/2ab(3−a−b)−9/2≥0{a^2} + {b^2} + {\left( {3 - a - b} \right)^2} + 3/2ab\left( {3 - a - b} \right) - 9/2 \ge 0

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

View graph