lean_workbook_plus_61820

Proved

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

If $X,Y,Z>0,X^2+Y^2+Z^2+XYZ=4,x=\frac{2X+YZ}{3YZ},y=\frac{2Y+ZX}{3ZX},z=\frac{2Z+XY}{3XY}$ then is the true relationship: $x,y,z>0,\frac{1}{x}+\frac{1}{y}+\frac{1}{z}=3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61820 (X Y Z x y z : ℝ) (hX : 0 < X) (hY : 0 < Y) (hZ : 0 < Z) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (h : X^2 + Y^2 + Z^2 + X * Y * Z = 4) (hn : x = (2 * X + Y * Z) / (3 * Y * Z)) (ho : y = (2 * Y + Z * X) / (3 * Z * X)) (hp : z = (2 * Z + X * Y) / (3 * X * Y)) : 1 / x + 1 / y + 1 / z = 3   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph