A formal proof of the Ramanujan--Nagell theorem in Lean 4

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,\pm 1),(4,\pm 3),(5,\pm 5),(7,\pm 11),(15,\pm 181)\}$. 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.