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.

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

License

BSD License

Topics

Session SumSquares

Cite

× 
@article{SumSquares-AFP,
  author  = {Roelof Oosterhuis},
  title   = {Sums of Two and Four Squares},
  journal = {Archive of Formal Proofs},
  month   = {August},
  year    = {2007},
  note    = {\url{https://isa-afp.org/entries/SumSquares.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: