Existing in Mathlib · Number theory

Lagrange's Four-Square Theorem

For every natural number n, there are four natural numbers—some of which may be zero—whose squares add exactly to n.

sum of squares
Euler four-square identity
prime descent
minimal multiplier
multiplicative induction

Exact theorem

Exact Mathlib statement

theorem Nat.sum_four_squares (n : ℕ) : ∃ a b c d : ℕ, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n

The theorem at a glance

Lagrange's Four-Square Theorem at a glance

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

An ivory number-theory poster shows exactly four square tiles, Euler multiplication rosettes, a shrinking prime multiplier, the four-square equation, five proof movements, and existence-only scope. — Every natural number has a representation as four natural-number squares, with zero terms allowed.

Statement structure

Statement and scope

Read the exact Mathlib declaration

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

Scientific figure illustrating: Euler multiplication and a least-multiplier prime descent assemble four-square representations for every natural number. — Euler multiplication and a least-multiplier prime descent assemble four-square representations for every natural number.

Why it matters

A mathematical landmark

Lagrange's theorem gives a universal additive representation of every natural number. Mathlib's proof combines Euler's four-square identity, prime descent, and multiplicative induction.

Proof architecture

Euler multiplication and Lagrange descent

5 curated stages

Mathlib proves that every natural number is a sum of four natural-number squares by establishing Euler's multiplicative identity, representing a multiple of each prime, descending a least positive multiplier to one, and extending prime representations to all naturals by multiplicative induction.

These source-anchored stages explain the retained Mathlib proof route. They are generated explanations, not proof evidence or an extracted Lean proof-term dependency graph.

Two four-square representations multiply into another
Two four-square representations multiply into another
Euler's identity combines two four-coordinate representations while preserving the sum-of-four-squares form of their product.
Open original image in a new tab
Euler's identity combines two four-coordinate representations while preserving the sum-of-four-squares form of their product.
(sum of four squares) · (sum of four squares) = sum of four squares
The proof first establishes Euler's four-square identity in a commutative ring and then a natural-number version using integer absolute values. This identity supplies the multiplicative step used both in prime descent and in the final induction.
Start with four squares equal to a small positive multiple of a prime
Start with four squares equal to a small positive multiple of a prime
A modular sum-of-two-squares argument yields a four-square representation of k p with the multiplier strictly between zero and p.
Open original image in a new tab
A modular sum-of-two-squares argument yields a four-square representation of k p with the multiplier strictly between zero and p.
0 < k < p and a²+b²+c²+d² = k p
For an odd prime, Mathlib uses a congruence for a sum of two squares modulo p, adds the square of one and the square of zero, and extracts a positive multiplier smaller than the prime. The prime two is handled directly.
Minimality prepares a smaller multiplier
Minimality prepares a smaller multiplier
Choose the least represented positive multiplier; halve it when even, or replace all four coordinates by least absolute residues when odd.
Open original image in a new tab
Choose the least represented positive multiplier; halve it when even, or replace all four coordinates by least absolute residues when odd.
m minimal; either m/2 or 0 < r < m
Nat.findX selects a minimal positive m with four squares equal to m p. If m is even, a parity lemma divides the representation by two. If m is odd, each coordinate is replaced by a congruent representative with absolute value less than half m, producing a positive quotient r<m.
The four-square identity completes the descent
The four-square identity completes the descent
Euler's identity combines the reduced residues with the original representation and, after division, represents r p, contradicting minimality.
Open original image in a new tab
Euler's identity combines the reduced residues with the original representation and, after division, represents r p, contradicting minimality.
m = 1; hence p = a²+b²+c²+d²
In the odd case, a reordered four-square representation of m r is multiplied by the representation of m p. The Euler outputs are all divisible by m; division yields a four-square representation of r p with r<m. Together with the even case, this makes every assumption m>1 impossible, so the prime itself is a sum of four squares.
Multiplicative induction reaches every natural number
Multiplicative induction reaches every natural number
Zero and one are immediate, primes use the descent, and products use Euler's identity, completing multiplicative induction.
Open original image in a new tab
Zero and one are immediate, primes use the descent, and products use Euler's identity, completing multiplicative induction.
∀ n : ℕ, ∃ a b c d : ℕ, a²+b²+c²+d²=n
Nat.sum_four_squares invokes Nat.recOnMul. The zero and one cases use representations with zero terms; the prime case invokes the theorem from page 4; and the product case combines two inductive representations with Euler's identity. Therefore every natural number has a four-square representation.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally

Locally reproducedExact upstream declaration replayed

Reviewed pageCurrent public presentation reviewed

Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

This target indexes Mathlib's existence theorem that every natural number is a sum of four squares of natural numbers. It does not count representations, require all four terms to be nonzero, or claim a new proof.

Proof Atlas did not originate Lagrange's Four-Square Theorem or Mathlib's declaration.
The theorem asserts existence only: it neither counts representations nor requires every term to be nonzero.
The generated explanation and visuals are not proof evidence.

Source and local evidence

Where the theorem comes from

Existing declaration: Nat.sum_four_squares in mathlib
Relationship: The checked artifact is the upstream declaration itself
Local Lean evidence: artifact.library.mathlib.lagrange-four-square-theorem.v001
Source: Open the pinned upstream reference

Exact Mathlib statement

Lagrange's Four-Square Theorem at a glance

Statement and scope

A mathematical landmark

Euler multiplication and Lagrange descent

Two four-square representations multiply into another

Start with four squares equal to a small positive multiple of a prime

Minimality prepares a smaller multiplier

The four-square identity completes the descent

Multiplicative induction reaches every natural number

What has been checked

No new theorem is claimed

Where the theorem comes from