A formal proof of the Ramanujan--Nagell theorem in Lean 4
This work provides a fully machine-checked proof of a classical number theory result, demonstrating the feasibility of formalizing complex algebraic number theory in Lean.
The authors formalized the Ramanujan-Nagell theorem in Lean 4, proving that the only integer solutions to x^2 + 7 = 2^n are the five known pairs. The formalization covers all necessary algebraic number theory, including ring of integers, class number, and unit group of Q(√-7).
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.