lean_workbook_plus_56265

Proved

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

Let $a=1+x,b=1+y,c=1+z,x,y,z\ge -1$ .Then $a^2+b^2+c^2+2abc+3-(1+a)(1+b)(1+c)=x^2+y^2+z^2+xyz.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_56265 (a b c x y z : ℝ) (ha : a = 1 + x) (hb : b = 1 + y) (hc : c = 1 + z) (hx : x ≥ -1) (hy : y ≥ -1) (hz : z ≥ -1) : a^2 + b^2 + c^2 + 2 * a * b * c + 3 - (1 + a) * (1 + b) * (1 + c) = x^2 + y^2 + z^2 + x * y * z   :=  by sorry

Source

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

View graph