Abstract
This document presents the mechanised proofs of the following results:
- any prime number of the form 4m+1 can be written as the sum of two squares;
- any natural number can be written as the sum of four squares