Existence: Lagrange's four square theorem

Fermat conjectured that every integer could be written as a sum of at most four squares. For example,

$$100 = 5^2 + 5^2 + 5^2 + 5^2$$

and

$$118 = 10^2 + 4^2 + 1^2 + 1^2$$

Lagrange managed to prove this conjecture to hold for all positive integers. Before we finalize our statement of Lagrange's Theorem, we make a simple observation. Consider a representation of an integer as a sum of fewer than four squares, e.g.

$$5 = 2^2 + 1^2$$

If we allow our squares to include zero, we can turn such a representation into a representation involving exactly four squares, e.g.

$$5 = 2^2 + 1^2 + 0^2 + 0^2$$

We use this observation to state Lagrange's Theorem in the following form:

Theorem (Lagrange's Four Square Theorem). Every positive integer has a representation as the sum of four squares.

This sort of result is what is generally known as an existance result as opposed to an enumeration. Although it tells us that such a representation must exist, it does not tell us how many such representations may be found.

Now it is possible to systematically write down and thus count all possible representations of a given positive integer as four squares. But this sort of approach is not always desirable, and, for some counting problems, not even feasible. For this particular problem, Jacobi managed to formally solve the enumeration problem without writing down solutions.