4. Sum of Two Squares
Fermat's theorem on sums of two squares (Fermat's Christmas theorem) states that every prime
p with p \equiv 1 \pmod 4 can be written as p = a^2 + b^2 with a, b \in \mathbb{N}.
Lean code for Definition4.1●1 definition
Associated Lean declarations
-
FermatSumOfTwoSquares[complete]
-
FermatSumOfTwoSquares[complete]
-
defdefined in DifferentProofs/SumOfTwoSquares/Defs.leancomplete
def FermatSumOfTwoSquares : Prop
def FermatSumOfTwoSquares : Prop
**Fermat's theorem on sums of two squares**: Every prime `p` congruent to `1` modulo `4` is a sum of two squares of natural numbers.
Two of the proofs below reduce the theorem to the same elementary descent: once -1 is known
to be a square modulo p, a pigeonhole argument recovers the two squares. They differ only in
how they exhibit a square root of -1.
Thue's descent: if -1 is a square modulo a prime p, then p = a^2 + b^2 for some
natural numbers a, b.
Lean code for Lemma4.2●1 theorem
Associated Lean declarations
-
theoremdefined in DifferentProofs/SumOfTwoSquares/Basic.leancomplete
theorem SumOfTwoSquares.sq_add_sq_of_isSquare_neg_one {p : ℕ} (hp : Nat.Prime p) (h : IsSquare (-1)) : ∃ a b, a ^ 2 + b ^ 2 = p
theorem SumOfTwoSquares.sq_add_sq_of_isSquare_neg_one {p : ℕ} (hp : Nat.Prime p) (h : IsSquare (-1)) : ∃ a b, a ^ 2 + b ^ 2 = p
**Thue's descent.** If `-1` is a square modulo a prime `p`, then `p` is a sum of two squares of natural numbers. The proof is a pigeonhole argument: with `r = ⌊√p⌋`, the `(r+1)²` pairs `(s, t)` with `0 ≤ s, t ≤ r` cannot inject into `ZMod p` via `(s, t) ↦ s - u·t`, where `u² = -1`; a collision yields `a, b` with `|a|, |b| ≤ r`, not both zero and `a² + b² ≡ 0`, whence `0 < a² + b² < 2p` forces `a² + b² = p`.
Fix u with u^2 \equiv -1 \pmod p and set r = \lfloor \sqrt p \rfloor. The
(r+1)^2 > p pairs (s, t) with 0 \le s, t \le r cannot map injectively into
\mathbb{Z}/p\mathbb{Z} under (s, t) \mapsto s - u t, so two distinct pairs collide. Their
difference (a, b) satisfies a \equiv u b \pmod p with |a|, |b| \le r and
(a, b) \ne (0, 0). Then a^2 + b^2 \equiv u^2 b^2 + b^2 \equiv 0 \pmod p, while
0 < a^2 + b^2 \le 2 r^2 < 2 p, forcing a^2 + b^2 = p.
First proof: quadratic reciprocity.
Every prime p \equiv 1 \pmod 4 is a sum of two squares.
Lean code for Theorem4.3●1 theorem
Associated Lean declarations
-
theoremdefined in DifferentProofs/SumOfTwoSquares/QuadraticReciprocity.leancomplete
theorem FermatSumOfTwoSquares_QuadraticReciprocity : FermatSumOfTwoSquares
theorem FermatSumOfTwoSquares_QuadraticReciprocity : FermatSumOfTwoSquares
Fermat's theorem on sums of two squares, via the first supplement to quadratic reciprocity.
The first supplement to quadratic reciprocity — equivalently Euler's criterion for the quartic
character \chi_4 — says that -1 is a square modulo an odd prime p iff
p \not\equiv 3 \pmod 4. This holds for p \equiv 1 \pmod 4, so the descent
Lemma 4.2 gives p = a^2 + b^2.
Second proof: Wilson's theorem.
Every prime p \equiv 1 \pmod 4 is a sum of two squares.
Lean code for Theorem4.4●1 theorem
Associated Lean declarations
-
FermatSumOfTwoSquares_Wilson[complete]
-
FermatSumOfTwoSquares_Wilson[complete]
-
theoremdefined in DifferentProofs/SumOfTwoSquares/Wilson.leancomplete
theorem FermatSumOfTwoSquares_Wilson : FermatSumOfTwoSquares
theorem FermatSumOfTwoSquares_Wilson : FermatSumOfTwoSquares
Fermat's theorem on sums of two squares, via Wilson's theorem: pairing `k` with `p - k` in `(p-1)! ≡ -1 (mod p)` shows that `(p/2)!` is a square root of `-1` when `p ≡ 1 (mod 4)`.
Wilson's theorem gives (p-1)! \equiv -1 \pmod p. Pairing each k with p - k rewrites
(p-1)! \equiv (-1)^{(p-1)/2}\bigl(((p-1)/2)!\bigr)^2 \pmod p. Since p \equiv 1 \pmod 4, the
exponent (p-1)/2 is even, so \bigl(((p-1)/2)!\bigr)^2 \equiv -1 \pmod p exhibits -1 as a
square, and the descent Lemma 4.2 gives p = a^2 + b^2.
Third proof: Zagier's "one-sentence" involution proof.
Every prime p \equiv 1 \pmod 4 is a sum of two squares.
Lean code for Theorem4.5●1 theorem
Associated Lean declarations
-
FermatSumOfTwoSquares_Zagier[complete]
-
FermatSumOfTwoSquares_Zagier[complete]
-
theoremdefined in DifferentProofs/SumOfTwoSquares/Zagier.leancomplete
theorem FermatSumOfTwoSquares_Zagier : FermatSumOfTwoSquares
theorem FermatSumOfTwoSquares_Zagier : FermatSumOfTwoSquares
**Zagier's one-sentence proof** of Fermat's theorem on sums of two squares.
Consider the finite set S = \{(x, y, z) \mid x, y, z > 0,\ x^2 + 4yz = p\}. The windmill
involution sends (x, y, z) to (x + 2z,\ z,\ y - x - z) when x < y - z, to
(2y - x,\ y,\ x - y + z) when y - z < x < 2y, and to (x - 2y,\ x - y + z,\ y) when
x > 2y; on S the boundary cases x = y - z and x = 2y are impossible because p is
prime. It has exactly one fixed point (namely (1, 1, (p-1)/4)), so |S| is odd. Therefore the
simple involution (x, y, z) \mapsto (x, z, y) must also have a fixed point (x, y, y), giving
x^2 + 4y^2 = p, i.e. p = x^2 + (2y)^2.
Fourth proof: Alpoge's proof via Jacobi sums.
Every prime p \equiv 1 \pmod 4 is a sum of two squares.
Lean code for Theorem4.6●1 theorem
Associated Lean declarations
-
FermatSumOfTwoSquares_Jacobi[complete]
-
FermatSumOfTwoSquares_Jacobi[complete]
-
theoremdefined in DifferentProofs/SumOfTwoSquares/Jacobi.leancomplete
theorem FermatSumOfTwoSquares_Jacobi : FermatSumOfTwoSquares
theorem FermatSumOfTwoSquares_Jacobi : FermatSumOfTwoSquares
Fermat's theorem on sums of two squares, via Jacobi sums: the Jacobi sum of a quartic character on `ZMod p` is a Gaussian integer of norm `p` (Alpoge's proof).
Let \chi_4 be a multiplicative character of \mathbb{Z}/p\mathbb{Z} of order 4 (it exists
because 4 \mid p - 1), taking values in the fourth roots of unity \mu_4 \subseteq \mathbb{C}.
The Jacobi sum J = \sum_x \chi_4(x)\,\chi_4(1 - x) then lies in \mathbb{Z}[i]. Because
\chi_4 and \chi_4^2 are nontrivial, J \cdot \overline{J} = p; writing J = a + b i
with a, b \in \mathbb{Z} gives a^2 + b^2 = p.