**This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.**

### 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