Prove2Me

lean_workbook_plus_4035

Proved

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

Let x=a−bx = a - b, y=b−cy = b - c, z=c−az = c - a. We have x+y+z=0x+y+z=0 and we have to prove 4(1+x2)(1+y2)(1+z2)≥(2+x2+y2+z2)24\left( {1 + {x^2}} \right)\left( {1 + {y^2}} \right)\left( {1 + {z^2}} \right) \ge {\left( {2 + {x^2} + {y^2} + {z^2}} \right)^2}

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

View graph