lean_workbook_plus_24212

Proved

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

Given $n = a^2 + b^2 + c^2$ , prove that $n^2 = x^2 + y^2 + z^2$ for some $x, y, z$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24212 {n : ℕ} (h : ∃ a b c : ℕ, n = a^2 + b^2 + c^2) : ∃ x y z : ℕ, n^2 = x^2 + y^2 + z^2   :=  by sorry

Source