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

Abstract

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.

v2: substantial revision; the Lean 4 formalization is rewritten to work directly in the Euclidean domain R = Z[(1+sqrt(-7))/2] rather than via the ring of integers of Q(sqrt(-7)), shortening it from ~3,570 to ~1,800 lines, with the exposition revised to match