Prove2Me

lean_workbook_plus_63117

Disproved

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

prove that: 3222(1−xyz)≥(1−x)(yz−1)+(1−y)(xz−1)+(1−z)(xy−1)≥0\frac{3^2}{2^2}(1-xyz) \geq (1-x)(yz-1)+(1-y)(xz-1)+(1-z)(xy-1)\geq 0

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

View graph