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

This paper presents a complete formalization of the Ramanujan–Nagell theorem in Lean 4, detailing the proof strategy, architectural design, and challenges involved in verifying the theorem's integer solutions through the computation of algebraic number theory concepts such as the ring of integers, class number, and unit group of $\mathbb{Q}(\sqrt{-7})$.

The Gist

Imagine you are a detective trying to solve a very specific, stubborn riddle left behind by a mathematical genius named Ramanujan in 1913.

The riddle is: "If you take a number, square it, add 7, and the result is a power of 2 (like 2, 4, 8, 16...), what numbers could you have started with?"

Ramanujan guessed the answers: $n$ could be 3, 4, 5, 7, or 15. He didn't prove there weren't any others. In 1948, a mathematician named Nagell finally proved that Ramanujan was right and that these are the only answers.

This paper is about a modern detective (Barinder Banwait) taking that old proof and translating it into a language that a computer can understand and verify with 100% certainty. The computer used is called Lean 4, and the massive library of math facts it uses is called Mathlib.

Here is the story of how they did it, explained simply.

1. The Goal: A Perfectly Locked Box

In the human world, mathematicians write proofs on paper. They say things like, "It is obvious that..." or "Clearly, this works." Sometimes, these "obvious" steps hide tiny logical gaps.

In the computer world, there is no "obvious." If you don't explain every single step, the computer stops and says, "I don't understand."

The author's goal was to build a digital fortress around this theorem. Every single brick of the argument had to be placed perfectly so the computer could check it and say, "Yes, this is true. There are no other solutions."

2. The Challenge: Speaking Two Languages

The biggest problem wasn't the math itself; it was the translation.

Think of the number system involved here (called $\mathbb{Q}(\sqrt{-7})$) as a special, exotic country. In this country, the "integers" (the whole numbers) aren't just 1, 2, 3. They are weird fractions involving square roots, like $\frac{1 + \sqrt{-7}}{2}$.

• The Paper Proof: The textbook proof treats this country like a familiar neighborhood. It assumes everyone knows the rules of the road.
• The Computer Proof: The computer is a tourist who has never been there. It needs a map, a dictionary, and a guide for every single street corner.

The author had to build the infrastructure from scratch. Before they could even start solving the riddle, they had to teach the computer:

• What the "integers" of this weird country actually look like.
• That this country has a special property called "Unique Factorization" (meaning every number breaks down into prime factors in only one way, like LEGO bricks).
• What the "units" (numbers that act like 1 or -1) are in this country.

Analogy: Imagine trying to prove a recipe works, but first, you have to invent the concept of "flour," build a mill to grind the wheat, and prove that flour is a solid substance before you can even talk about mixing it into a cake. That's what the first half of this paper does.

3. The Strategy: The Detective's Toolkit

Once the computer understood the "country," the author applied the same logic Nagell used in 1948, but with extreme precision.

• Step 1: The Even Case. If the power of 2 is even, the math is simple. The computer checks this quickly and finds the answer $n=4$.
• Step 2: The Odd Case. If the power is odd, things get tricky. The author had to break the equation down into pieces using a "binomial expansion" (a fancy way of multiplying out brackets).
• Step 3: The Modulo Magic. The author used a trick called "modulo arithmetic" (like looking at a clock). They showed that the answer $n$ could only be a few specific types of numbers (like numbers that leave a remainder of 3, 5, or 13 when divided by 42).
• Step 4: The Final Blow. They proved that even within those specific types, there could only be one answer for each type.

4. The "Glue" and the "AI Assistant"

This is where the story gets modern.

The "Glue" (Typeclass Diamonds):
In computer logic, sometimes two different ways of defining the same thing (like two different maps to the same city) don't automatically match up. The computer gets confused and says, "These look different to me!" The author had to write special code to force the computer to realize, "Hey, these are actually the same thing." It's like realizing that a "soda" and a "pop" are the same drink, even though the labels are different.

The AI Assistant:
The author didn't do this alone. They used Generative AI (like a super-smart coding intern).

• The Tactic: When the author got stuck, the AI suggested the next logical step.
• The Repair: When the computer library updated and changed some names, the AI fixed the broken code automatically.
• The Search: Finding the right mathematical rule in a library with millions of entries is like finding a needle in a haystack. The AI found the needles instantly.

Important Note: The AI didn't write the proof. It just helped the human write it faster. The computer (Lean) still checked every single line to make sure the AI didn't hallucinate a lie.

5. Why Does This Matter?

You might ask, "Who cares if a computer checked a math problem from 1948?"

• Certainty: In math, human error happens. We miss a step or make a calculation mistake. A computer check is absolute. If the computer says it's true, it is true.
• The Future: This is the first time a famous conjecture by Ramanujan has been fully verified by a computer. It proves that we can now use computers to verify the most complex, abstract branches of mathematics.
• The Blueprint: The author didn't just solve the problem; they built a "blueprint" (a map of the code) that other mathematicians can use to solve other hard problems in the future.

Summary

Think of this paper as the story of a master architect (the author) who took a beautiful, old house (the Ramanujan-Nagell theorem) and rebuilt it using indestructible, transparent glass.

They had to invent new tools to cut the glass, hire a robot assistant to help with the heavy lifting, and spend months ensuring every single pane was perfectly aligned. The result? A house that no one can ever doubt is standing on solid ground.

Technical Summary

1. Problem Statement

The paper addresses the Ramanujan–Nagell theorem, a classic result in number theory concerning the Diophantine equation:
$$x^2 + 7 = 2^n$$
where $x$ and $n$ are integers.

• The Claim: The only integer solutions $(n, x)$ are:
  $$(n, x) \in \{(3, \pm1), (4, \pm3), (5, \pm5), (7, \pm11), (15, \pm181)\}$$
• Context: Originally posed by Srinivasa Ramanujan in 1913 and proved by Trygve Nagell in 1948, the proof relies on algebraic number theory, specifically the arithmetic of the quadratic field $K = \mathbb{Q}(\sqrt{-7})$.
• Goal: To provide a complete, machine-checked formalization of this theorem and its underlying infrastructure within the Lean 4 interactive theorem prover using the Mathlib library.

2. Methodology

The formalization follows the standard mathematical proof (based on Stewart and Tall) but requires rigorous translation into Lean's type theory. The methodology involves three main layers:

A. Mathematical Strategy

The proof is divided into two cases based on the parity of $n$:

1. Even Case ($n$ is even): The equation factors over integers as $(2^{n/2} + x)(2^{n/2} - x) = 7$. Since 7 is prime, this yields a unique solution ($n=4, x=\pm3$).
2. Odd Case ($n$ is odd): The equation is rewritten in the ring of integers $\mathcal{O}_K$ of $K = \mathbb{Q}(\sqrt{-7})$.
   • The ring $\mathcal{O}_K$ is identified as $\mathbb{Z}[\theta]$ where $\theta = \frac{1+\sqrt{-7}}{2}$.
   • The equation becomes a factorization: $\left(\frac{x+\sqrt{-7}}{2}\right)\left(\frac{x-\sqrt{-7}}{2}\right) = \theta^m \theta'^m$ (where $m = n-2$).
   • Using the fact that $\mathcal{O}_K$ is a Unique Factorization Domain (UFD) and has only units $\pm 1$, the problem reduces to solving $\pm\sqrt{-7} = \theta^m - \theta'^m$.
   • A binomial expansion and reduction modulo 7 restrict $m$ to specific residue classes modulo 42.
   • A uniqueness argument using 7-adic valuations proves that each residue class yields at most one solution.

B. Formalization Architecture

The project consists of 3,570 lines of code across five files, organized into two layers:

1. Algebraic Infrastructure (3 files): Establishes the properties of $\mathcal{O}_K$.
   • QuadraticIntegerROI.lean: General theory for rings of integers of $\mathbb{Q}(\sqrt{d})$ where $d \equiv 1 \pmod 4$.
   • RingOfIntegers.lean: Specializes to $d = -7$.
   • FieldIsomorphism.lean: Bridges the gap between the "natural" field presentation $\mathbb{Q}(\sqrt{-7})$ and the integral basis presentation $\mathbb{Q}(\theta)$.
2. Proof Core (2 files):
   • Helpers.lean: Computes invariants (discriminant, class number, unit group) and proves irreducibility of $\theta$.
   • Basic.lean: Contains the main theorem, the mod-42 reduction, and the uniqueness proof.

C. Key Technical Challenges

• Type Isomorphism: Lean's QuadraticAlgebra type distinguishes between $\mathbb{Q}(\sqrt{-7})$ (generator $\omega^2 = -7$) and $\mathbb{Q}(\frac{1+\sqrt{-7}}{2})$ (generator $\omega^2 = -2 + \omega$). The formalization required constructing an explicit $\mathbb{Q}$-algebra isomorphism to transport the "integral closure" property between these distinct types.
• Unit Group Determination: Proving the unit group is $\{\pm 1\}$ required leveraging Dirichlet's Unit Theorem (available in Mathlib) and performing a computationally intensive case analysis to rule out roots of unity of order 3, 4, and 6.
• Arithmetic in $\mathcal{O}_K$: Standard integer tactics (like linarith) do not work in $\mathcal{O}_K$. The author had to manually coerce elements to the field $K$, simplify, and prove identities, often requiring explicit handling of subtypes and integrality proofs.
• Binomial Expansion: The reduction modulo 42 required complex manipulation of finite sums (Finset.sum_filter, sum_bij) to separate even and odd terms and reindex indices.

3. Key Contributions

1. First Formalization of a Ramanujan Conjecture: This is the first time a conjecture posed by Ramanujan has been fully formalized in a proof assistant.
2. First Complete Resolution of an Exponential Diophantine Equation: It represents the first complete machine-checked resolution of a specific exponential Diophantine equation in any formal verification system.
3. New Algebraic Number Theory Infrastructure: The project contributes reusable code for:
   • Identifying the ring of integers for quadratic fields with $d \equiv 1 \pmod 4$.
   • Computing class numbers and unit groups for specific quadratic fields.
   • Handling isomorphisms between different presentations of the same number field.
4. AI-Assisted Workflow Analysis: The paper documents the use of generative AI (Claude Code and Aristotle) in the formalization process, demonstrating how AI can assist with tactic suggestion, proof repair, lemma discovery, and boilerplate generation.

4. Results

• Theorem Verified: The main theorem RamanujanNagell was proven without any sorry (unproven) axioms. It depends only on the three standard Lean axioms: propext, Classical.choice, and Quot.sound.
• Dependencies: The proof relies on Mathlib's IsPrincipalIdealRing, UniqueFactorizationDomain, padicValNat, and Dirichlet's Unit Theorem.
• Performance: The formalization required significant computational resources for certain steps (e.g., setting maxHeartbeats to 400,000 for unit group analysis), highlighting that while the logic is standard, the computational cost of formalizing arithmetic in number rings is high.

5. Significance

• Bridging the Gap: The paper highlights the substantial "gap" between textbook proofs and formal proofs. Concepts that are "obvious" or "standard" in mathematics (e.g., identifying the ring of integers, handling unit groups, or performing arithmetic in $\mathcal{O}_K$) require hundreds of lines of code and intricate type-level reasoning in Lean.
• Infrastructure Reusability: The algebraic infrastructure developed (specifically for quadratic fields) is designed to be generalizable, aiding future formalizations of other Diophantine equations.
• Role of AI: The paper serves as a case study for the future of formal verification. It suggests that AI tools are becoming essential for managing the complexity and boilerplate of large-scale formalizations, potentially lowering the barrier to entry for mathematicians entering the field of formal verification.
• Mathlib Growth: By porting and extending results from the Brasca–Monticone library and integrating them with Mathlib, this work strengthens the ecosystem for algebraic number theory in Lean 4.

In conclusion, this work is a milestone in formal mathematics, demonstrating that complex, classical number theory results can be fully verified in modern proof assistants, provided that sufficient infrastructure is built and that new tools (like AI) are leveraged to manage the inherent complexity of the formalization process.