lean_workbook_plus_67101

Proved

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

Let $x,y,z$ are real number such that $xyz=-1$ Prove that $3(x^2-x+1)(y^2-y+1)(z^2-z+1) \geq 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67101 (x y z : ℝ) (h : x*y*z = -1) :
  3 * (x^2 - x + 1) * (y^2 - y + 1) * (z^2 - z + 1) ≥ 1   :=  by sorry

Source