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

TL;DR

This paper provides a complete formal proof of the Ramanujan--Nagell theorem using Lean 4, including detailed algebraic number theory formalizations and proof strategies.

Contribution

It introduces a comprehensive formalization of the theorem in Lean 4, covering algebraic number theory dependencies and proof architecture.

Findings

Formal proof confirms all known solutions to the equation

Includes formalization of quadratic field ring of integers and class number

Addresses challenges in translating textbook proofs to formal proof

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,\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.