Lagrange 在 1770 年证明的四平方定理大概是数论里最好讲的"美感与机械之间"的例子之一： 结论一句话就说完——每个自然数都是四个整数的平方和——而经典证明里却塞了两块完全不同的工具，一个是 Euler 的代数恒等式，一个是 Fermat 的下降法。 这两件东西怎样和当代的 Lean / Mathlib 形式化对应，是这篇笔记想理一理的事。

1. 经典证明

定理本身写出来是

要求 $a,b,c,d \in \mathbb{N}$ 也是等价的，因为负号在平方时被吃掉。

证明的第一根柱子是 Euler 四平方恒等式：

这条等式说：“四平方和"对乘法封闭。它把整个问题约化为只证素数情形：如果每个素数都是四平方和，那么由素因子分解和上述乘法封闭，所有正整数都是。

接下来证素数 $p$。$p=2$ 用 $2 = 1^2 + 1^2 + 0^2 + 0^2$ 直接结束。对奇素数 $p$，先证一个"初始倍数"引理：存在整数 $a, b$ 和 $m$，使得

构造很自然。在 $\mathbb{F}_p$ 里看两个集合

每个集合都有 $(p+1)/2$ 个元素。它们的并集大小不可能超过 $p$，所以必然相交。 于是存在 $a, b$ 使 $a^2 \equiv -1 - b^2 \pmod p$，即 $p \mid a^2 + b^2 + 1$。 把 $a, b$ 选成最小绝对值代表元，就有 $0 < m < p$。

下一步是 Fermat 的下降法。取最小的正整数 $m$ 使得 $m p = a^2 + b^2 + c^2 + d^2$ 有解。 $m = 1$ 时素数情形完成。假设 $m > 1$，我们要导出 $r < m$ 的更小见证，与 $m$ 的最小性矛盾。

$m$ 为偶数时简单。从 $a^2+b^2+c^2+d^2 = 2M$ 把 $a,b,c,d$ 按奇偶配对， 同奇偶的 $x, y$ 满足

所以 $M$ 仍是四个整数的平方和。应用到 $m p = 2 \cdot (m/2) \cdot p$，得到 $(m/2) p$ 是四平方和，违背 $m$ 的最小性。

$m$ 为奇数时把 $a, b, c, d$ 分别换成模 $m$ 的最小绝对值代表元 $A, B, C, D$，使 $|A|, |B|, |C|, |D| < m/2$。 原式被 $m$ 整除，所以

对某个非负整数 $r$。绝对值估计给 $0 \le r < m$。 $r$ 不会是零：如果 $A=B=C=D=0$，那么 $m$ 同时整除 $a,b,c,d$，于是 $m^2 \mid m p$， 即 $m \mid p$，与 $1 < m < p$ 矛盾。所以 $0 < r < m$。

最后再请出 Euler 恒等式，把 $A^2+B^2+C^2+D^2 = rm$ 和原 $a^2+b^2+c^2+d^2 = mp$ 相乘。 通过恰当选择符号，恒等式给出的四个线性组合都同时被 $m$ 整除， 除以 $m^2$ 后得到

且 $0 < r < m$，与 $m$ 的最小性矛盾。因此 $m = 1$，奇素数 $p$ 是四平方和。

2. Lean 4 / Mathlib 中的形式化

Mathlib 的对应文件是 Mathlib.NumberTheory.SumFourSquares，主定理写成

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

素数版本是

protected theorem Nat.Prime.sum_four_squares {p : ℕ} (hp : p.Prime) :
    ∃ a b c d : ℕ, a^2 + b^2 + c^2 + d^2 = p

Euler 恒等式作为前置工具单独存在：euler_four_squares 对任意交换环成立， 自然数版 Nat.euler_four_squares 用 Int.natAbs 把可能带负号的中间表达式拉回 $\mathbb{N}$。

一段最常见的使用 sketch 看上去是这样的：

import Mathlib.NumberTheory.SumFourSquares

open scoped BigOperators

def FourSq (n : ℕ) : Prop :=
  ∃ a b c d : ℕ, a^2 + b^2 + c^2 + d^2 = n

example (n : ℕ) : FourSq n :=
  Nat.sum_four_squares n

example {p : ℕ} (hp : Nat.Prime p) : FourSq p :=
  hp.sum_four_squares

-- 乘法封闭：用 Euler 恒等式把两个见证拼成一个
theorem FourSq.mul {m n : ℕ} (hm : FourSq m) (hn : FourSq n) :
    FourSq (m * n) := by
  rcases hm with ⟨a, b, c, d, hm⟩
  rcases hn with ⟨x, y, z, w, hn⟩
  refine ⟨
    ((a : ℤ) * x - b * y - c * z - d * w).natAbs,
    ((a : ℤ) * y + b * x + c * w - d * z).natAbs,
    ((a : ℤ) * z - b * w + c * x + d * y).natAbs,
    ((a : ℤ) * w + b * z - c * y + d * x).natAbs,
    ?_⟩
  calc
    _ = (a^2 + b^2 + c^2 + d^2) * (x^2 + y^2 + z^2 + w^2) := by
        simpa using Nat.euler_four_squares a b c d x y z w
    _ = m * n := by rw [hm, hn]

Mathlib 主证明并不显式遍历素因子表。它用的是 Nat.recOnMul： “如果你能证 $P(0)$、$P(1)$、所有素数 $p$ 的 $P(p)$、以及乘法步 $P(m) \wedge P(n) \Rightarrow P(mn)$， 那么 $P$ 对所有自然数都成立”。源码的最终分支正是 zero / one / prime / mul 四个 case， 其中乘法 case 调用 euler_four_squares。这把"素因子分解 + 乘法封闭"的纸面句式直接转成 induction principle。

3. 形式化里几个真正的难点

存在性的粒度。 纸面证明随手就说"两个大小为 $(p+1)/2$ 的集合在 $\mathbb{F}_p$ 里必相交”。 要在 Lean 里手写出来，需要 Fintype.card、Finset.image、平方映射在代表元上的单射性、抽屉原理一整套基础设施。 Mathlib 没有重写，直接调有限域里的现成结果 ZMod.sq_add_sq，再用 Nat.sq_add_sq_zmodEq 把它翻译成带代表元估计的自然数命题。

下降法的编码。 Lean 不接受"无限下降所以矛盾"这种纸面口号。要把它形式化成"取最小反例"。 Mathlib 里用 Nat.findX 把最小的 $m$ 取出来，再每次构造 $r < m$ 的新见证， 直接喂给最小性假设产生 contradiction。这与纸面证明结构一致，但所有"存在最小"和"严格小于"的细节都要写明。

$\mathbb{N}$ 与 $\mathbb{Z}$ 的反复切换。 Euler 恒等式里那四个线性组合天然带减号，在 $\mathbb{Z}$ 中自然， 但目标命题在 $\mathbb{N}$。Mathlib 的解决方法是用 .natAbs^2，证明里大量用 push_cast、norm_cast、sq_abs、mod_cast 来回搬运。 偶数情形还得处理"除以 2"：Int.sq_add_sq_of_two_mul_sq_add_sq 把 $2m = x^2 + y^2$ 转成 $m = ((x-y)/2)^2 + ((x+y)/2)^2$，这一步先要证奇偶性才能保证整除。

形式化的体感是：纸面证明里几行就过去的存在性、最小性、奇偶估计、平方差， 在 Lean 里每一步都得点出对应的引理名字，但每一步都对得上。 两块工具——Euler 恒等式管乘法，Fermat 下降管素数——在 Mathlib 里仍然清楚可见。 Lagrange 的原始证明结构经过两百多年，至今仍是这个定理被验证、被讲、被形式化的标准路径。

积土成山，风雨兴焉；积水成渊，蛟龙生焉。——荀子《劝学》