Three Squares Theorem

Anton Danilkin and Loïc Chevalier

May 3, 2023

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

We formalize the Legendre's three squares theorem and its consequences, in particular the following results:
  1. A natural number can be represented as the sum of three squares of natural numbers if and only if it is not of the form $4^a (8 k + 7)$, where $a$ and $k$ are natural numbers.
  2. If $n$ is a natural number such that $n \equiv 3 \pmod{8}$, then $n$ can be be represented as the sum of three squares of odd natural numbers.
Consequences include the following:
  1. An integer $n$ can be written as $n = x^2 + y^2 + z^2 + z$, where $x$, $y$, $z$ are integers, if and only if $n \geq 0$.
  2. The Legendre's four squares theorem: any natural number can be represented as the sum of four squares of natural numbers.

License

BSD License

Topics

Session Three_Squares