1 The Ramanujan–Nagell Theorem
The Ramanujan–Nagell equation is the Diophantine equation
where \(x\) is an integer and \(n\) is a natural number. The theorem, conjectured by Ramanujan and proved by Nagell, states that the only solutions are \((x, n) \in \{ (\pm 1, 3),\; (\pm 3, 4),\; (\pm 5, 5),\; (\pm 11, 7),\; (\pm 181, 15)\} \).
The proof splits into two cases depending on the parity of \(n\): the even case uses a factorization argument over \(\mathbb {Z}\), while the odd case requires algebraic number theory in the ring of integers of \(\mathbb {Q}(\sqrt{-7})\).
1.1 Setup: the quadratic ring \(R = \mathbb {Z}[(1+\sqrt{-7})/2]\)
We work directly in the quadratic algebra
the free \(\mathbb {Z}\)-module on \(1\) and a generator \(\theta \) with \(\theta ^2 = \theta - 2\). Concretely \(R = \mathbb {Z}[(1+\sqrt{-7})/2]\), the ring of integers of \(\mathbb {Q}(\sqrt{-7})\), with \(\theta = (1+\sqrt{-7})/2\) and its conjugate \(\theta ' = (1-\sqrt{-7})/2\). In Lean these are the top-level definitions \(\theta = \langle 0, 1\rangle \) and \(\theta ' = \langle 1, -1\rangle \); there is no separate field \(K\), integral closure, or class-number computation.
The quadratic ring \(R = \texttt{QuadraticAlgebra}\; \mathbb {Z}\; (-2)\; 1 = \mathbb {Z}[(1+\sqrt{-7})/2]\).
Proof in Lean source.
The generator \(\theta = \langle 0, 1\rangle = (1+\sqrt{-7})/2 \in R\).
Proof in Lean source.
The conjugate \(\theta ' = \langle 1, -1\rangle = (1-\sqrt{-7})/2 \in R\).
Proof in Lean source.
The following identities are all definitional (rfl) in \(R\).
\(\theta ^2 = \theta - 2\).
Definitional.
\(\theta \cdot \theta ' = 2\).
Definitional.
\(\theta + \theta ' = 1\).
Definitional.
\(\theta ' = 1 - \theta \).
Definitional.
For \(x, y \in \mathbb {Z}\), the norm of \(\langle x, y\rangle \in R\) is \(N(\langle x, y\rangle ) = x^2 + xy + 2y^2\).
Unfold the quadratic-algebra norm and simplify.
For all \(z \in R\), \(0 \leq N(z)\). (The norm form \(x^2 + xy + 2y^2 = \tfrac 14\big((2x+y)^2 + 7y^2\big)\) is positive definite.)
Complete the square: \(4N(\langle x,y\rangle ) = (2x+y)^2 + 7y^2 \geq 0\).
For \(z \in R\), \(N(z) = 0\) if and only if \(z = 0\).
\(4N(\langle x,y\rangle ) = (2x+y)^2 + 7y^2\) vanishes only when \(x = y = 0\).
The only units in \(R\) are \(\pm 1\).
A unit has norm \(1\). From \(4N(\langle x,y\rangle ) = (2x+y)^2 + 7y^2\), the equation \(N(\langle x,y\rangle ) = 1\) forces \(y = 0\) and \(x = \pm 1\), so the unit is \(\pm 1\).
In \(R\), we have \(\theta \cdot (1 - \theta ) = 2\), i.e. \(\frac{1+\sqrt{-7}}{2} \cdot \frac{1-\sqrt{-7}}{2} = 2\).
Proof in Lean source.
1.1.1 \(R\) is a unique factorization domain
Rather than going through discriminants, class numbers, and Dirichlet’s unit theorem, we establish unique factorization in \(R\) directly, via the chain
\(R\) is a Euclidean domain, with the norm \(N\) as Euclidean function. To divide \(a\) by \(b \neq 0\) we round \(a \cdot \bar{b} / N(b)\) by a smart scheme (round the \(\sqrt{-7}\) coordinate first, then shift-round the rational part), which yields a remainder with \(16\, N(\mathrm{rem}) \leq 11\, N(b)\), hence of strictly smaller norm.
Proof in Lean source.
Every ideal of \(R\) is principal, since every Euclidean domain is a principal ideal ring.
Proof in Lean source.
\(R\) is a unique factorization domain, since every principal ideal ring is one.
Proof in Lean source.
Combined with \(N(\theta ) = N(\theta ') = 2\) (so \(\theta , \theta '\) have prime norm), this gives that \(\theta \) and \(\theta '\) are irreducible, hence prime (Lemmas 54, 52, 56, 53).
1.2 The even case
When \(n\) is even, say \(n = 2k\), the equation becomes \(x^2 + 7 = 2^{2k}\), which factors over \(\mathbb {Z}\) as \((2^k + x)(2^k - x) = 7\). Since \(7\) is prime, this forces \(n = 4\) and \(x = \pm 3\).
If \((2^k + x)(2^k - x) = 7\), then either \(2^k - x = 1\) and \(2^k + x = 7\), or \(2^k - x = 7\) and \(2^k + x = 1\).
Both factors are positive integers whose product is the prime \(7\), so one factor is \(1\) and the other is \(7\).
1.3 The odd case
When \(n\) is odd and \(n \geq 5\), the proof works in the ring of integers of \(\mathbb {Q}(\sqrt{-7})\). Setting \(m = n - 2\), we divide the equation by \(4\) to obtain \((x^2 + 7)/4 = 2^m\), which factors in \(R\) as \(\theta ^m \cdot \theta '^{\, m}\). The conjugate factors \((x \pm \sqrt{-7})/2\) lie in \(R\) (since \(x\) is odd) and their product equals \(\theta ^m \cdot \theta '^{\, m}\). Using unique factorization and coprimality, one deduces the key identity \(-2\theta + 1 = \theta ^m - \theta '^{\, m}\).
1.3.1 Exercises: from factorization to sign condition
The proof of the main \(m\)-condition is structured as a chain of four lemmas (exercises), followed by a sign-determination step.
The conjugate factors \((x \pm \sqrt{-7})/2\) lie in \(R\) (since \(x\) is odd), and their product equals \(\theta ^m \cdot \theta '^{\, m}\). Their difference is \(2\theta - 1 = \sqrt{-7}\).
Express the factors using \(\theta \) and \(\theta '\), verify the product using \(\theta \cdot \theta ' = 2\), and compute the difference.
The conjugate factors are coprime in \(R\). The only prime factors of \(2\) in \(R\) are \(\theta \) and \(\theta '\) (since \(2 = \theta \cdot \theta '\)). If either divided both factors, it would divide their difference \(\sqrt{-7}\), but \(N(\sqrt{-7}) = 7\) is not divisible by \(N(\theta ) = N(\theta ') = 2\).
Norm argument: any common factor divides \(\sqrt{-7}\), whose norm is \(7\), incompatible with the norm \(2\) of \(\theta \) and \(\theta '\).
If \(\alpha \cdot \beta = \theta ^m \cdot \theta '^{\, m}\) and \(\gcd (\alpha , \beta ) = 1\) in the UFD \(R\), then \(\alpha = \pm \theta ^m\) or \(\alpha = \pm \theta '^{\, m}\). This combines unique factorization in \(R\) (UniqueFactorizationMonoid) with the fact that the only units are \(\pm 1\) (units_pm_one).
Proof in Lean source.
From \(\alpha = \pm \theta ^m\) or \(\alpha = \pm \theta '^{\, m}\), use the product relation to determine \(\beta \), then take the difference \(\alpha - \beta = 2\theta - 1\) to eliminate \(x\) and obtain: either \(2\theta - 1 = \theta ^m - \theta '^{\, m}\) or \(-2\theta + 1 = \theta ^m - \theta '^{\, m}\).
Case split on the four possibilities for \(\alpha \), determine \(\beta \) from the product, and compute \(\alpha - \beta \).
If either \(2\theta - 1 = \theta ^m - \theta '^{\, m}\) or \(-2\theta + 1 = \theta ^m - \theta '^{\, m}\) holds for odd \(m \geq 3\), then in fact the minus sign must hold: \(-2\theta + 1 = \theta ^m - \theta '^{\, m}\). This is proved by reducing modulo \(\theta '^2\) and checking which sign is consistent.
Reduce modulo \(\theta '^2\) and verify only the minus sign is consistent.
1.3.2 Key intermediate result
For all integers \(x\) and odd \(m \geq 3\), if \((x^2 + 7)/4 = 2^m\), then
Chain the exercises: construct the conjugate factors, prove coprimality, apply UFD association, eliminate \(x\), then determine the sign.
1.3.3 From the \(m\)-condition to finitely many solutions
If \(n\) is odd with \(n \geq 5\) and \(x^2 + 7 = 2^n\), then \((x^2 + 7)/4 = 2^{n-2}\).
Since \(n \geq 5\), we have \(4 \mid 2^n\), so divide both sides by \(4\).
From \(-2\theta + 1 = \theta ^m - \theta '^{\, m}\), expand via the binomial theorem and reduce modulo \(7\) to obtain \(-2^{m-1} \equiv m \pmod{7}\).
The proof multiplies both sides by \(2^m\), expands \((1 + \sqrt{-7})^m - (1 - \sqrt{-7})^m\) via the binomial theorem, observes that even-index terms cancel and odd-index terms involve powers of \((\sqrt{-7})^2 = -7\), then reads the result modulo \(7\).
Binomial expansion and reduction modulo \(7\).
If \(n\) is odd with \(n \geq 5\) and \(x^2 + 7 = 2^n\), then \((-2)^{n-3} \equiv n - 2 \pmod{7}\).
This follows from the \(m\)-condition (Lemma 22) by expanding \(\theta ^m - \theta '^{\, m}\) via the binomial theorem and reducing modulo \(7\).
Combine the reduction and binomial expansion lemmas.
If \(n\) is odd with \(n \geq 5\) and \(x^2 + 7 = 2^n\), then \((n - 2) \bmod 42 \in \{ 3, 5, 13\} \).
This follows from \((-2)^{n-3} \equiv n - 2 \pmod{7}\) together with Fermat’s little theorem \(2^6 \equiv 1 \pmod{7}\). Checking residues modulo \(42\) (combining mod \(6\) and mod \(7\)) yields the three residue classes.
Exhaustive check of residues modulo \(42\) using the mod \(7\) constraint and Fermat’s little theorem.
1.3.4 Uniqueness per residue class
The mod \(42\) constraint narrows \(m = n - 2\) to three residue classes. To show that each class contains at most one solution, we use a \(7\)-adic argument.
Define the odd-indexed binomial sum
This arises from expanding \((1+\sqrt{-7})^d = A_d + \sqrt{-7} \cdot B_d\).
Proof in Lean source.
The \(7\)-adic valuation of \(B_d\) equals \(v_7(d)\): if \(7^l \| d\) (i.e. \(7^l \mid d\) but \(7^{l+1} \nmid d\)), then \(7^l \mid B_d\) and \(7^{l+1} \nmid B_d\).
This is the core of the \(7\)-adic analysis: the \(j=0\) term of \(B_d\) equals \(d\), and all higher terms have strictly larger \(7\)-adic valuation.
The \(j=0\) term is \(d\) with valuation \(l\). Each \(j \geq 1\) term has \(7\)-adic valuation \(\geq l+1\), so by the ultrametric property the sum has valuation exactly \(l\).
Define the even-indexed binomial sum
This arises from the even-index part of the expansion of \((1+\sqrt{-7})^d\).
Proof in Lean source.
If \(7^l \| d\) and \(7 \mid d\), then \(7^l \mid A'_d\) and \(7^{l+1} \nmid A'_d\). The \(j=0\) term \(\binom {d}{2} = d(d-1)/2\) has valuation \(l\), and all higher terms have strictly larger \(7\)-adic valuation.
Same structure as for \(B_d\): the leading term \(\binom {d}{2}\) has valuation \(l\), and higher terms are absorbed.
Define the integer recurrence \(a(0) = 2\), \(a(1) = 1\), \(a(n+2) = a(n+1) - 2\, a(n)\). This is the trace sequence: \(a(n) = \theta ^n + \theta '^{\, n}\) in \(R\).
Proof in Lean source.
For all \(n\), \(\mathrm{trace\_ seq}(n) = \theta ^n + \theta '^{\, n}\) in \(R\).
Induction on \(n\) using the recurrence, with \(\theta + \theta ' = 1\) and \(\theta \cdot \theta ' = 2\).
For all \(n\), \(7 \nmid a(n)\). The recurrence has period \(3\) modulo \(7\), and the three residues \(a(0) \equiv 2\), \(a(1) \equiv 1\), \(a(2) \equiv -3\) are all nonzero mod \(7\).
Show the recurrence is periodic mod \(7\) with period \(3\), then check all three residues.
For natural numbers, \(n\) is even if and only if \(n\) is not odd.
Immediate from not_odd_iff_even.
If \(m_1, m_2\) are both odd, \(\geq 3\), satisfy \(m_1 \equiv m_2 \pmod{42}\), and both give \(-2\theta + 1 = \theta ^{m_i} - \theta '^{\, m_i}\), then \(m_1 = m_2\).
Proof sketch: if \(m_1 \neq m_2\), let \(d = |m_2 - m_1|\), which is divisible by \(42\) (hence by \(7\)). The \(7\)-adic analysis of Lemma 28 combined with Corollary C yields a contradiction on the valuation of \(\sqrt{-7} \cdot B_d\).
Contradiction via \(7\)-adic valuation: \(d\) is divisible by \(42\) (hence \(7\)), and the valuation identity forces an impossible parity.
1.3.5 Verification of known solutions
\(-2\theta + 1 = \theta ^3 - \theta '^{\, 3}\). Verified via \(x = 5\): \((25 + 7)/4 = 8 = 2^3\).
Direct computation using \(\theta ^2 = \theta - 2\).
\(-2\theta + 1 = \theta ^5 - \theta '^{\, 5}\). Verified via \(x = 11\): \((121 + 7)/4 = 32 = 2^5\).
Direct computation using \(\theta ^2 = \theta - 2\).
\(-2\theta + 1 = \theta ^{13} - \theta '^{\, 13}\). Verified via \(x = 181\): \((32761 + 7)/4 = 8192 = 2^{13}\).
Direct computation using \(\theta ^2 = \theta - 2\).
1.3.6 Combining
If \(n\) is odd with \(n \geq 5\) and \(x^2 + 7 = 2^n\), then \(n \in \{ 5, 7, 15\} \).
From the mod \(42\) constraint, \(m = n - 2\) lies in one of three residue classes (\(3\), \(5\), or \(13\) mod \(42\)). The verification lemmas show these are actual solutions (at \(m = 3, 5, 13\)). The uniqueness lemma shows each residue class has at most one solution. Therefore \(n \in \{ 5, 7, 15\} \).
Combine the mod \(42\) constraint, uniqueness per class, and verification of the three known solutions.
1.4 Main theorem
1.4.1 Direct computation
Once the possible values of \(n\) are determined (either by the even-case factorization or the odd-case modular argument), it remains to solve for \(x\) by direct computation. A single generic lemma handles all five cases: it takes an equation \(x^2 = a^2\) (where \(a^2 = 2^n - 7\)) and the value of \(n\), and identifies the solution pair \((x, n)\).
If \(x^2 = a^2\) and \(n = m\), then \((x, n) = (a, m)\) or \((x, n) = (-a, m)\).
From \(x^2 = a^2\) we get \(x = a\) or \(x = -a\).
1.4.2 The theorem
The only integer solutions to \(x^2 + 7 = 2^n\) are
First, one shows \(n \geq 3\) by bounding \(2^n \geq x^2 + 7 \geq 7\).
Case 1: \(n\) even. Write \(n = 2k\). Then \((2^k+x)(2^k-x) = 7\). By Lemma 16, the only possibility is \(2^k = 4\), giving \(n = 4\) and \(x = \pm 3\) (Lemma 40).
Case 2: \(n\) odd, \(n = 3\). Direct computation gives \(x^2 = 1\), so \(x = \pm 1\) (Lemma 40).
Case 3: \(n\) odd, \(n \geq 5\). By Theorem 39, \(n \in \{ 5, 7, 15\} \), and direct computation gives the remaining solutions (Lemma 40).
1.5 Additional declarations
TODO: add description
Proof in Lean source.
TODO: add description
Proof in Lean source.
TODO: add description
Proof in Lean source.
The conjugate factors ‘(x ± √-7)/2‘ lie in ‘R‘ (since ‘x‘ is odd) and
Proof in Lean source.
TODO: add description
Proof in Lean source.
The integer ring ‘ℤ[(1 + √-7)/2]‘, packaged as ‘QuadraticAlgebra ℤ (-2) 1‘. -/
Proof in Lean source.
TODO: add description
Proof in Lean source.
The integer ring ‘ℤ[(1 + √-7)/2]‘, packaged as ‘QuadraticAlgebra ℤ (-2) 1‘. -/
Proof in Lean source.
TODO: add description
Proof in Lean source.
TODO: add description
Proof in Lean source.
TODO: add description
Proof in Lean source.
TODO: add description
Proof in Lean source.
TODO: add description
Proof in Lean source.
The integer ring ‘ℤ[(1 + √-7)/2]‘, packaged as ‘QuadraticAlgebra ℤ (-2) 1‘. -/
Proof in Lean source.
The integer ring ‘ℤ[(1 + √-7)/2]‘, packaged as ‘QuadraticAlgebra ℤ (-2) 1‘. -/
Proof in Lean source.
TODO: add description
Proof in Lean source.