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

Barinder S. Banwait

arxiv: 2604.09808 · v2 · pith:G3TA4ONPnew · submitted 2026-04-10 · 🧮 math.NT · cs.LO

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

Barinder S. Banwait This is my paper

Pith reviewed 2026-05-10 16:09 UTC · model grok-4.3

classification 🧮 math.NT cs.LO

keywords Ramanujan-Nagell theoremLean 4formal verificationDiophantine equationquadratic fieldclass numberunit group

0 comments

The pith

A complete Lean 4 formalization establishes that x squared plus 7 equals 2 to the n only for the five listed solution pairs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper delivers a full machine-checked proof in Lean 4 of the Ramanujan-Nagell theorem, which asserts that the Diophantine equation x squared plus 7 equals 2 to the n has only the integer solutions with n and x equal to the pairs 3 and plus or minus 1, 4 and plus or minus 3, 5 and plus or minus 5, 7 and plus or minus 11, and 15 and plus or minus 181. The formalization incorporates every required dependency, such as the explicit computation of the ring of integers of the quadratic field Q of square root of negative 7, along with that field's class number and unit group. This work translates an existing textbook argument into a form that the Lean system can verify independently. A sympathetic reader would value the result because it supplies an independently checkable guarantee that no other integer solutions exist.

Core claim

The paper presents a complete formalization in Lean 4 with Mathlib of the Ramanujan-Nagell theorem stating that the only integer solutions to x squared plus 7 equals 2 to the n are the pairs (n, x) in the set with n equals 3 and x plus or minus 1, n equals 4 and x plus or minus 3, n equals 5 and x plus or minus 5, n equals 7 and x plus or minus 11, and n equals 15 and x plus or minus 181. The formalization covers the full proof strategy together with all supporting algebraic number theory facts about the field Q of square root of negative 7.

What carries the argument

The Lean 4 formalization of the ring of integers, class number, and unit group of the quadratic field Q of square root of negative 7, which carries the descent and bounding arguments that restrict the possible exponents n.

If this is right

The listed solution pairs are now available as a verified lemma inside Lean for direct reuse in other formal proofs.
The supporting infrastructure for quadratic fields, rings of integers, class numbers, and unit groups becomes part of the permanent Mathlib library.
Textbook proofs that rely on similar algebraic number theory can be translated into machine-checked form using the same techniques.
The documented challenges show precisely where informal proofs must be expanded to meet the requirements of interactive theorem provers.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same formalization approach could be applied to other exponential Diophantine equations whose proofs use class-group computations.
Once the quadratic-field tools exist, they lower the barrier for formalizing further results that depend on unique factorization in quadratic rings.
The explicit recording of every definition and lemma makes it possible to extract a human-readable outline of the proof that matches the original textbook steps.

Load-bearing premise

The Lean code correctly encodes the textbook definitions and proof steps for the quadratic field and the Diophantine argument without introducing or omitting any logical content.

What would settle it

An explicit integer pair (n, x) satisfying x squared plus 7 equals 2 to the n that lies outside the five listed pairs, or a detected error in the Lean code that severs the chain of verified implications from the field properties to the solution list.

Figures

Figures reproduced from arXiv: 2604.09808 by Barinder S. Banwait.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Banwait has produced a complete Lean 4 formalization of the Ramanujan-Nagell theorem that includes the full algebraic number theory setup for Q(sqrt(-7)).

read the letter

Banwait has produced a complete Lean 4 formalization of the Ramanujan-Nagell theorem that includes the full algebraic number theory setup for Q(sqrt(-7)). The listed solutions are now machine-checked down to Mathlib axioms, with explicit handling of the ring of integers, class number, and unit group. That is the main deliverable here. The theorem itself has been known since the 1940s, so the paper adds no new mathematical content. Its value sits in the verified artifact and the reusable infrastructure it contributes to the library. The write-up describes the proof strategy and the practical gaps between textbook arguments and formal code, which is useful for anyone trying similar work. The approach follows standard Mathlib patterns for quadratic fields, and the stress-test found no load-bearing problems. Soundness rests on the type checker rather than on new arguments. One minor limitation is that the paper focuses on one specific equation, so the broader impact on algebraic number theory formalization remains incremental. Without the code itself it is hard to judge the exact encoding choices, but nothing in the description raises red flags. This work is aimed at people who track Lean developments or want a verified reference for this Diophantine result. A reader already familiar with formal methods will get the most out of it. The paper is coherent on its own terms and shows clear engagement with the literature on both the theorem and the formalization side. It deserves a serious referee because formalizations of this scope need external checking for completeness and library integration. I would send it to peer review rather than desk reject.

Referee Report

0 major / 1 minor

Summary. The manuscript presents a complete formalization in Lean 4 (with Mathlib) of the Ramanujan-Nagell theorem: the only integer solutions to the equation x² + 7 = 2ⁿ are the pairs (n, x) ∈ {(3, ±1), (4, ±3), (5, ±5), (7, ±11), (15, ±181)}. The formalization includes the full algebraic-number-theoretic infrastructure (ring of integers of ℚ(√-7), its class number, and unit group) together with the Diophantine argument, and describes the proof strategy, architecture, and encoding challenges.

Significance. If the encoding is faithful, the result is significant because it supplies a machine-checked proof that reduces directly to the axioms of Lean and Mathlib with no free parameters, fitted data, or circular definitions. The work also contributes reusable formalizations of quadratic-field primitives that have already appeared in other Mathlib developments, thereby lowering the barrier for future formalizations of similar Diophantine results.

minor comments (1)

The description of the proof architecture would benefit from an explicit listing of the main Lean files or modules and their dependencies, so that readers can locate the formalization of the class-number computation and the descent step without searching the repository.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of our manuscript and for recommending acceptance. We are pleased that the contribution of the complete Lean 4 formalization of the Ramanujan--Nagell theorem, including the supporting algebraic number theory infrastructure, is recognized as significant.

Circularity Check

0 steps flagged

No circularity: deductive formalization to Lean/Mathlib axioms

full rationale

The paper delivers a complete Lean 4 formalization of the Ramanujan-Nagell theorem, encoding the full Diophantine argument together with explicit computations of the ring of integers of Q(√-7), its class number, and unit group. All steps reduce directly to the axioms and definitions in Mathlib (already used in other quadratic-field formalizations) with no fitted parameters, self-referential definitions, predictions that loop back to input data, or load-bearing self-citations. The central claim holds by construction once the code type-checks, making the derivation self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The formalization rests on the standard axioms of mathematics as implemented in Lean 4 together with the pre-existing Mathlib formalizations of quadratic fields, class groups, and units; no free parameters, ad-hoc axioms, or new entities are introduced.

axioms (2)

standard math Axioms of mathematics as encoded in Lean 4
All formal proofs ultimately rest on these foundational axioms.
domain assumption Correctness of Mathlib implementations for quadratic fields, class numbers, and unit groups
The proof depends on these library components for the algebraic number theory parts.

pith-pipeline@v0.9.0 · 5432 in / 1373 out tokens · 57223 ms · 2026-05-10T16:09:06.395929+00:00 · methodology

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

Core claim

What carries the argument

If this is right

Where Pith is reading between the lines

Load-bearing premise

What would settle it

discussion (0)