Prove2Me

lean_workbook_plus_3940

Proved

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

Let x,yx, y , and zz be real numbers satisfying x+y+z=xyzx + y + z = xyz. Prove that x(1−y2)(1−z2)+y(1−z2)(1−x2)+z(1−x2)(1−y2)=4xyz.x(1 - y^2)(1 - z^2) + y(1 -z^2)(1 - x^2) + z(1 - x^2)(1 - y^2) = 4xyz.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3940 (x y z : ℝ) (h : x + y + z = x*y*z) :
  x * (1 - y ^ 2) * (1 - z ^ 2) + y * (1 - z ^ 2) * (1 - x ^ 2) + z * (1 - x ^ 2) * (1 - y ^ 2) = 4*x*y*z   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph