lean_workbook_plus_50566

Proved

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

For $n\geq 2$ , if $a,\ b$ satisfy $a^2 + b^2 = 2^n$ , then prove that both $a$ and $b$ are even.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50566 (n a b : ℕ) (ha : a^2 + b^2 = 2^n) (hb : 2 ≤ n) : Even a ∧ Even b   :=  by sorry

Source