Theorem Marketplace

Theorem Details

import Mathlib

theorem four_squares (n : Nat) : ∃ (a b c d : Nat), n = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 := 
  sorry

Bounty: 0.0003 ETH

Status: Closed

Proof

import Mathlib

theorem four_squares (n : Nat) : ∃ (a b c d : Nat), n = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 := by
  have ⟨a,b,c,d,h⟩ := Nat.sum_four_squares n
  use a ; use b ; use c ; use d
  rw [h]

Back to Bounties