TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Lagrange's four-square theorem: every nonnegative integer is a sum of four integer squares

Statement

Every nonnegative integer is a sum of four integer squares. That is, for every integer $n \geq 0$ there is a quadruple $(a, b, c, d) \in Z^{4}$ with $n = a^{2} + b^{2} + c^{2} + d^{2}$ (Representations as sums of four squares).

Facts & Assumptions

Given: The nonnegative integers.

[F1]

A representation of a nonnegative integer $n$ as a sum of four squares is an ordered quadruple $(a, b, c, d) \in Z^{4}$ with $n = a^{2} + b^{2} + c^{2} + d^{2}$ (Representations as sums of four squares).

[F2]

For $d, a \in Z$ , $d ∣ a$ means $a = d q$ for some $q \in Z$ (Divisibility in $Z$ : $d ∣ a$ when $a = d q$ for some integer $q$ ).

[F3]

An integer $p$ is prime when $p > 1$ and $d ∣ p$ with $d > 0$ force $d = 1$ or $d = p$ (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ).

[L1]

Every prime is a sum of four integer squares. (Every prime is a sum of four integer squares).

[L2]

Let $m$ and $n$ be nonnegative integers; if each of $m$ and $n$ is a sum of four integer squares, then $m n$ is a sum of four integer squares (Sums of four squares are closed under products).

[L3]

Let $n \in Z$ with $n > 1$ and put $S : = {d \in Z : d ∣ n and d > 1}$ . Then $S$ is nonempty and has a least element $q$ , and $q$ is prime; in particular every integer greater than $1$ has a prime divisor (Every integer $n > 1$ has a prime divisor; indeed the least divisor of $n$ that exceeds $1$ is prime).

[L4]

Let $S \subseteq Z$ be nonempty. If $S$ has an upper bound, it has a greatest element; if $S$ has a lower bound, it has a least element. In each case the element is unique (A nonempty set of integers bounded above has a greatest element, and a nonempty set of integers bounded below has a least element).

Proof

technique · contradiction

1.1

Suppose, for contradiction, that not every nonnegative integer is a sum of four integer squares.

assume-contra

2.1

Let $T$ be the set of nonnegative integers that are not sums of four integer squares; by step 1.1 it is nonempty, and it is bounded below by $0$ , so [L4] gives it a least element $n_{0}$ .

step 1.1L4F1construct

3.1

Neither $0$ nor $1$ lies in $T$ , since $0 = 0^{2} + 0^{2} + 0^{2} + 0^{2}$ and $1 = 1^{2} + 0^{2} + 0^{2} + 0^{2}$ are representations in the sense of [F1]; as $n_{0} \in T$ and $n_{0} \geq 0$ , this forces $n_{0} > 1$ .

step 2.1F1algebra

4.1

By [L3] the integer $n_{0} > 1$ has a prime divisor $q$ , and by [F2] there is an integer $k$ with $n_{0} = q k$ .

step 3.1L3F2choose

5.1

Here $k \geq 1$ , since $k \leq 0$ would give $n_{0} = q k \leq 0$ against $n_{0} > 1$ ; and $k < n_{0}$ , since step 4.1 gives $q$ prime, so [F3] gives $q > 1$ , hence $q \geq 2$ , and therefore $n_{0} = q k \geq 2 k = k + k > k$ .

step 4.1F3algebra

6.1

Since $0 \leq k < n_{0}$ and $n_{0}$ is least in $T$ , the integer $k$ is not in $T$ , so $k$ is a sum of four integer squares; and $q$ is a sum of four integer squares by [L1].

step 2.1step 5.1L1

7.1

Both factors of $n_{0} = q k$ are nonnegative and are sums of four integer squares, so [L2] makes $n_{0}$ one, contradicting $n_{0} \in T$ ; the assumption of step 1.1 therefore fails, and every nonnegative integer is a sum of four integer squares.

step 4.1step 6.1L2F1discharge-contradiction∎

Remarks

Why $0$ and $1$ are treated by hand. The proof factors $n_{0}$ through a prime divisor, and neither small value has one: $1$ is a product of no primes at all and $0$ is not a product of primes. Both are covered instead by the explicit quadruples in step 3.1, which the definition admits because coordinates may vanish.

Negative integers are outside the statement, not an omission. A square is nonnegative, and so is any sum of squares, so no negative integer is a sum of four integer squares, and the hypothesis $n \geq 0$ is the exact range where the conclusion can hold.

Four is not improvable. Some integers admit no representation with a vanishing coordinate, so they are not sums of three squares. The proposition Positive integers $4^{a} m$ with $m \equiv 7 (m o d 8)$ are not sums of three integer squares and its corollary Positive integers $4^{a} m$ with $m \equiv 7 (m o d 8)$ need four nonzero squares exhibit the family $4^{a} m$ with $m \equiv 7 (m o d 8)$ ; they do not assert the converse classification.

Depends on

Used by

Dependency tree · two levels

27 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

MIT 18.781 Theory of Numbers, Lecture 22, Theorem 80 (standard reference, not scraped)
Karl-Dieter Crisman, Number Theory: In Context and Interactive, §14.2, Fact 14.2.2 (standard reference, not scraped)