We present a complete formalization, in the Lean interactive theorem prover with the Mathlib library, of the Ramanujan--Nagell theorem: the only integer solutions to the Diophantine equation $x^2 + 7 = 2^n$ are $(n,x) \in \{(3,\pm1),(4,\pm3),(5,\pm5),(7,\pm11),(15,\pm181)\}$. The formalization includes all dependencies, notably the computation of the ring of integers of the quadratic field $\mathbb{Q}(\sqrt{-7})$, its class number, and unit group. We describe the proof strategy, the architecture of the formalization, and the challenges encountered in bridging the gap between textbook proofs and their machine-checked counterparts, with particular attention to the algebraic number theory infrastructure required.

翻译：我们在Lean交互式定理证明器及Mathlib库中，给出了Ramanujan-Nagell定理的完整形式化：丢番图方程$x^2 + 7 = 2^n$仅有的整数解为$(n,x) \in \{(3,\pm1),(4,\pm3),(5,\pm5),(7,\pm11),(15,\pm181)\}$。形式化过程涵盖了所有依赖，特别是二次域$\mathbb{Q}(\sqrt{-7})$的整数环计算、其类数及单位群的确定。我们描述了证明策略、形式化的体系结构，以及在弥合教科书证明与其机器检查版本之间差距时遇到的挑战，尤其关注所需的代数数论基础架构。