Lean 4 中 Ramanujan--Nagell 定理的形式化证明

我们在 Lean interactive theorem prover 以及 Mathlib library 中，对 Ramanujan--Nagell 定理进行了完整的 formalization：该定理指出，Diophantine 方程 $x^2 + 7 = 2^n$ 的唯一整数解为 $(n,x) \in \{(3,\pm1),(4,\pm3),(5,\pm5),(7,\pm11),(15,\pm181)\}$。该 formalization 包括所有依赖项，尤其是计算二次域 $\mathbb{Q}(\sqrt{-7})$ 的整数环、其 class number 和 unit group。我们描述了 proof strategy、formalization 的 architecture，以及在桥接 textbook proofs 与 machine-checked 版本之间的挑战，特别关注所需的 algebraic number theory 基础设施。