Sums of Two and Four Squares

Roelof Oosterhuis

August 12, 2007

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


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


BSD License


Session SumSquares