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

- Mathematics/Number theory

### Session Three_Squares

- Residues_Properties
- Low_Dimensional_Linear_Algebra
- Quadratic_Forms
- Three_Squares

### Depends on

- Dirichlet L-Functions and Dirichlet’s Theorem

### Used by

- Wieferich–Kempner Theorem
- Polygonal Number Theorem

### Auto-related entries

- Positional Notation for Natural Numbers in an Arbitrary Base
- Digit Expansions
- Dirichlet Series
- Sums of Two and Four Squares
- From THE BOOK: Two Squares via Involutions

## Cite

×

Three_Squares-AFP

    @article{Three_Squares-AFP,
      author  = {Anton Danilkin and Loïc Chevalier},
      title   = {Three Squares Theorem},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2023},
      note    = {\url{https://isa-afp.org/entries/Three_Squares.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- May 16, 2023 : Isabelle2022