Lagrange's Four-Squares theorem

Write a function that returns, for any natural, a list of four other naturals, the sum of the squares of which is the given natural. 

Function Signature

def four_squares (x : Nat) : List Nat

Theorem Signature

theorem is_valid (x : Nat) : (four_squares x).length = 4 ∧ ((four_squares x).map (fun a => a * a)).sum = x

View All Submissions

Please log in or register to submit a solution for this challenge.