Prove2Me

lean_workbook_plus_11790

Proved

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

Given that x+y+z=7x+y+z=7 , xy+yz+xz=10xy+yz+xz=10 and xyz=5xyz=5 , compute (2−x)(2−y)(2−z)(2-x)(2-y)(2-z) .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_11790 (x y z : ℝ) (hx : x + y + z = 7) (hy : x*y + y*z + z*x = 10) (hz : x*y*z = 5) : (2 - x) * (2 - y) * (2 - z) = -5   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph