lean_workbook_plus_1901

Proved

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

Note that: $a^{2}+b^{2}+c^{2}+2abc+1-2(ab+bc+ca)= (a-1)^{2}+(b-1)^{2}+(c-1)^{2}+2(a-1)(b-1)(c-1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1901 (a b c : ℝ) : a^2 + b^2 + c^2 + 2*a*b*c + 1 - 2*(a*b + b*c + a*c) = (a-1)^2 + (b-1)^2 + (c-1)^2 + 2*(a-1)*(b-1)*(c-1)   :=  by sorry

Source

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

View graph