lean_workbook_plus_21315

Proved

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

Given $a + b + c = 0$ , show that $2a^4 + 2b^4 + 2c^4$ is a perfect square.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_21315 (a b c : ℤ) (h : a + b + c = 0) : ∃ k : ℤ, k^2 = 2 * a^4 + 2 * b^4 + 2 * c^4   :=  by sorry

Source