Prove2Me

lean_workbook_plus_23935

Proved

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

If x1,x2,x3∈Rx_1,x_2,x_3\in\mathbb{R} such that x1+x2+x3=0,x_1+x_2+x_3=0, then\nx1x2x3≥x1x2+x2x3+x3x1−(x1x2+x2x3+x3x1)2x_1x_2x_3\ge{x_1x_2+x_2x_3+x_3x_1-(x_1x_2+x_2x_3+x_3x_1)^2}

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

View graph