Prove2Me

lean_workbook_plus_1464

Proved

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

We have P=x2+y2+z2=1(1+a)2+1(1+b)2+1(1+c)2 P= x^2+y^2+z^2 =\frac1{(1+a)^2}+\frac1{(1+b)^2}+\frac1{(1+c)^2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1464 (x y z a b c : ℝ) (hx : x = 1 / (1 + a)) (hy : y = 1 / (1 + b)) (hz : z = 1 / (1 + c)) : x ^ 2 + y ^ 2 + z ^ 2 = 1 / (1 + a) ^ 2 + 1 / (1 + b) ^ 2 + 1 / (1 + c) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph