Prove2Me

lean_workbook_plus_36950

Disproved

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

prove that: x2+y2+z2+x+y+z≥x2+y2+z2+3≥2(xy+xz+yz)x^2+y^2+z^2+x+y+z\geq x^2+y^2+z^2+3\geq2(xy+xz+yz)

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

View graph