lean_workbook_plus_23841

Proved

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

Let $A_i=b_i+c_i$ , $B_i=a_i+c_i$ , $C_i=a_i+b_i$ and $s_i=a_i+b_i+c_i$ . It is easy to see that $a_i^2+b_i^2+c_i^2+s_i^2=A_i^2+B_i^2+C_i^2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23841 (a b c s A B C : ℕ → ℕ) (hA : A = b + c) (hB : B = a + c) (hC : C = a + b) (hs : s = a + b + c) : a^2 + b^2 + c^2 + s^2 = A^2 + B^2 + C^2   :=  by sorry

Source

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

View graph