Prove2Me

lean_workbook_plus_14869

Disproved

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

(x1+x2+x3)2≥9+3x3(x1+x2+x3−3)+2x1x2−2x32(x_1+x_2+x_3)^2 \ge 9+ 3x_3(x_1+x_2+x_3-3)+2x_{1}x_2-2x_3^2

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

View graph