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.

Every prime is a sum of four integer squares

Statement

Every prime is a sum of four integer squares. That is, for every prime $p$ (Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$ ) there is a quadruple $(a, b, c, d) \in Z^{4}$ with $p = a^{2} + b^{2} + c^{2} + d^{2}$ (Representations as sums of four squares).

Facts & Assumptions

Given: A prime $p$ .

[F1]

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$ ).

[F2]

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).

[L1]

For every prime $p$ there is an integer $m$ with $1 \leq m < p$ for which $p m$ is a sum of four integer squares (Some multiple $p m$ with $1 \leq m < p$ is a sum of four squares).

[L2]

If $p$ is prime, $1 < m < p$ and $p m$ is a sum of four integer squares, then there is an integer $n$ with $1 \leq n < m$ for which $p n$ is a sum of four integer squares (Descent step: a smaller multiple of $p$ is a sum of four squares).

[L3]

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 the prime $p$ is not a sum of four integer squares.

assume-contra

1.2

Let $S$ be the set of integers $m$ with $1 \leq m < p$ for which $p m$ is a sum of four integer squares; $S$ is nonempty by [L1].

givenF1F2L1construct

2.1

The set $S$ is bounded below by $1$ , so [L3] gives it a least element $m_{0}$ , and $1 \leq m_{0} < p$ because $m_{0} \in S$ .

step 1.2L3

3.1

The value $m_{0} = 1$ is impossible: it would make $p = p \cdot 1$ a sum of four integer squares, against step 1.1. Hence $m_{0} > 1$ , and with step 2.1 this gives $1 < m_{0} < p$ .

step 1.1step 2.1F2algebra

4.1

Applying [L2] to the prime $p$ and the multiplier $m_{0}$ , whose hypotheses $1 < m_{0} < p$ and " $p m_{0}$ is a sum of four integer squares" are step 3.1 and membership of $m_{0}$ in $S$ , gives an integer $n$ with $1 \leq n < m_{0}$ for which $p n$ is a sum of four integer squares.

step 2.1step 3.1L2

5.1

Then $1 \leq n < m_{0} < p$ , so $n \in S$ while $n < m_{0}$ , contradicting the leastness of $m_{0}$ ; the assumption of step 1.1 therefore fails, and $p$ is a sum of four integer squares.

step 2.1step 4.1F2algebradischarge-contradiction∎

Remarks

What makes the descent terminate. The proof does not iterate the descent lemma; it applies it once, to the least multiplier, and reads the contradiction off leastness. The least element is supplied by [L3], for a set of integers bounded below, so no appeal to an infinite descending chain is needed and no infinite regress is written.

Where the hypothesis that $p$ is prime enters. Twice, through [L1] and through [L2]. In [L1] it supplies the congruence and the bound $p \geq 2$ used to obtain a multiplier below $p$ ; in the construction underlying [L2] it is used when a positive divisor of $p$ is forced to be $1$ or $p$ . For a composite modulus the multiplier can stall above $1$ , so the statement proved here is genuinely about primes; the passage from primes to all nonnegative integers is Lagrange's four-square theorem: every nonnegative integer is a sum of four integer squares, and it uses Sums of four squares are closed under products rather than a further descent.

Depends on

Used by

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

Dependency tree · two levels

28 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

Keith Conrad, Proofs by Descent, §6, Theorem 6.6 (standard reference, not scraped)
MIT 18.781 Theory of Numbers, Lecture 22, Theorem 80 (standard reference, not scraped)