Papers With

← All papers
First page of A formal proof of the Ramanujan--Nagell theorem in Lean 4

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

Barinder S. Banwait

math.NT Apr 10, 2026 · v1
formalization mathlib number-theory
Read PDF arXiv abstract Code
TL;DR
Complete Lean + Mathlib formalization of the Ramanujan-Nagell theorem and its number-theory dependencies.
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.
Problem

The Ramanujan-Nagell theorem (the only integer solutions to x^2 + 7 = 2^n) had no machine-checked formal proof. Formalizing it requires substantial algebraic number theory infrastructure including rings of integers, class numbers, and unit groups of quadratic fields.

Approach

The formalization in Lean 4 with Mathlib proves that Q(sqrt(-7)) is norm-Euclidean (rather than using class number one) to obtain unique factorization directly from the Euclidean algorithm, which is considerably easier to formalize. The development includes the ring of integers Z[(1+sqrt(-7))/2], its norm function, norm-Euclidean property, and unit group computation.

Results

A complete machine-checked proof of the Ramanujan-Nagell theorem: the only integer solutions to x^2 + 7 = 2^n are (n,x) in {(3,+/-1),(4,+/-3),(5,+/-5),(7,+/-11),(15,+/-181)}. The formalization comprises two files built directly on Mathlib, with an interactive dependency graph and proof blueprint publicly available.