English
For every natural number n, there exist a,b,c,d ∈ ℕ with a^2 + b^2 + c^2 + d^2 = n.
Русский
Для каждого натурального числа n существуют a,b,c,d ∈ ℕ такие, что a^2 + b^2 + c^2 + d^2 = n.
LaTeX
$$$\forall n \in \mathbb{N},\quad \exists a,b,c,d \in \mathbb{N},\ a^2 + b^2 + c^2 + d^2 = n$$$
Lean4
/-- **Four squares theorem** -/
theorem sum_four_squares (n : ℕ) : ∃ a b c d : ℕ, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n := by
-- The proof is by induction on prime factorization. The case of prime `n` was proved above,
-- the inductive step follows from `Nat.euler_four_squares`.
induction n using Nat.recOnMul with
| zero => exact ⟨0, 0, 0, 0, rfl⟩
| one => exact ⟨1, 0, 0, 0, rfl⟩
| prime p hp => exact hp.sum_four_squares
| mul m n hm hn =>
rcases hm with ⟨a, b, c, d, rfl⟩
rcases hn with ⟨w, x, y, z, rfl⟩
exact ⟨_, _, _, _, euler_four_squares _ _ _ _ _ _ _ _⟩
