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

Dieser Artikel beschreibt die vollständige formale Verifizierung des Satzes von Ramanujan–Nagell in Lean 4 unter Verwendung der Mathlib-Bibliothek, wobei insbesondere die erforderliche Infrastruktur der algebraischen Zahlentheorie sowie die Herausforderungen bei der Übertragung klassischer Beweise in maschinengeprüfte Formate beleuchtet werden.

Das Wesentliche

Stellen Sie sich vor, Mathematik ist wie ein riesiges, altes Schloss voller Geheimnisse. Seit über 100 Jahren versuchen die klügsten Köpfe der Welt, eine bestimmte Tür in diesem Schloss zu öffnen. Diese Tür ist eine mathematische Gleichung, die der berühmte indische Genie-Ramanujan im Jahr 1913 aufgestellt hat.

Die Frage war einfach: Welche Zahlen ergeben, wenn man sie quadriert und 7 addiert, eine reine Zweierpotenz? (Also Zahlen wie 2, 4, 8, 16, 32, 64...).

Ramanujan fand fünf Lösungen. Er vermutete aber: „Das sind die einzigen." Niemand konnte das beweisen, bis 1948 ein Mann namens Nagell die Tür endlich aufschloss.

Jetzt kommt die Geschichte von Barinder S. Banwait ins Spiel. Er hat diese Tür nicht nur mit dem menschlichen Verstand geöffnet, sondern sie vollständig von einem Computer überprüfen lassen. Er hat den Beweis in eine Sprache übersetzt, die ein Computer versteht: Lean 4.

Hier ist eine einfache Erklärung, was er getan hat, mit ein paar lustigen Vergleichen:

1. Der Beweis als Bauplan

Stellen Sie sich den mathematischen Beweis wie einen Bauplan für ein Haus vor. Ein normaler Mathematiker schreibt: „Nehmen Sie eine Wand, setzen Sie ein Fenster ein." Das reicht für Menschen.
Ein Computer aber ist wie ein extrem pedantischer Bauinspektor. Er fragt: „Was genau ist ein Fenster? Aus welchem Material? Ist die Wand senkrecht? Haben Sie den Fundament-Check gemacht?"

Banwait musste also nicht nur den Beweis schreiben, sondern das gesamte Fundament neu gießen. Er musste dem Computer beibringen, was eine „Zahl" ist, was ein „Ring" ist (eine spezielle Art von Zahlenmenge) und wie man mit komplexen Zahlen rechnet, die Wurzeln aus negativen Zahlen enthalten.

2. Die Reise in eine fremde Welt (Der Ring der ganzen Zahlen)

Um die Tür zu öffnen, mussten die Mathematiker in eine andere Dimension reisen: den Bereich der Zahlen, die man sich wie ein Gitter vorstellen kann, aber mit einer Wurzel aus -7.

• Das Problem: In der menschlichen Mathematik sagt man einfach: „Okay, wir arbeiten jetzt in diesem Gitter."
• Das Computer-Problem: Für den Computer sind zwei Darstellungen desselben Gitters wie zwei verschiedene Sprachen. Eine sagt „Wir nutzen die Wurzel aus -7", die andere sagt „Wir nutzen (1 + Wurzel aus -7) geteilt durch 2".
• Die Lösung: Banwait musste dem Computer einen Übersetzer bauen. Er hat eine Brücke geschlagen, die dem Computer zeigt: „Hey, diese beiden Welten sind eigentlich identisch, auch wenn sie anders aussehen." Ohne diesen Übersetzer hätte der Computer den Beweis nicht verstehen können.

3. Der Detektiv-Teil (Die Einzigartigkeit)

Der eigentliche Beweis hat zwei Teile:

1. Die Suche: Finde alle möglichen Kandidaten.
2. Die Überprüfung: Beweise, dass es keine weiteren Kandidaten gibt.

Hier kommt ein spannendes Werkzeug ins Spiel: Die 7-adische Bewertung.
Stellen Sie sich vor, Sie suchen nach einem bestimmten Schlüssel in einem Haufen von Schlüsseln. Sie wissen, dass der Schlüssel, den Sie suchen, eine bestimmte Anzahl von „7-Teilen" hat.
Der Beweis zeigt: Wenn Sie einen Kandidaten finden, der fast passt, aber nicht ganz, dann muss er sich von einem anderen Kandidaten um eine riesige Zahl unterscheiden. Aber die Mathematik sagt: „Nein, das ist unmöglich!"
Es ist wie ein Detektiv, der sagt: „Wenn der Täter heute hier war, müsste er morgen dort sein. Aber er kann nicht an beiden Orten gleichzeitig sein. Also war er gar nicht hier."

4. Warum ist das so schwer für Computer?

Im menschlichen Mathematikunterricht springen wir oft über kleine Details hinweg. Wir sagen: „Das ist offensichtlich."
Für einen Computer ist „offensichtlich" oft eine Falle.

• Beispiel: Wenn Sie im Kopf rechnen, wissen Sie, dass 2 + 2 = 4. Im Computer muss man beweisen, dass die Art und Weise, wie man die 2 definiert, wirklich zur 4 führt.
• Die Herausforderung: Banwait musste tausende von winzigen Schritten beweisen, die ein Mensch als „einfach" abtun würde. Er hat den Computer gezwungen, jeden einzelnen Ziegelstein zu prüfen.

5. Der neue Helfer: Künstliche Intelligenz (KI)

Ein besonders spannender Teil dieser Arbeit ist, dass Banwait KI als Assistenten benutzt hat.
Stellen Sie sich vor, Sie versuchen, ein riesiges Puzzle zu legen. Normalerweise suchen Sie stundenlang nach dem richtigen Teil.
Mit der KI (wie Claude Code oder Aristotle) ist es so, als hätte man einen Freund, der sofort sagt: „Probier mal diesen Teil hier aus!" oder „Ah, du hast einen Fehler in der Anleitung gemacht, hier ist die korrekte Version."
Die KI hat nicht den Beweis erfunden (das hat der Mensch getan), aber sie hat die langweilige, mühsame Arbeit des Suchens und Korrigieren enorm beschleunigt.

Das Fazit

Dieses Papier ist ein Meilenstein. Es ist das erste Mal, dass eine so komplexe Vermutung von Ramanujan vollständig von einem Computer verifiziert wurde.
Es zeigt uns, dass wir in eine Ära eintreten, in der wir nicht nur auf das Vertrauen in unsere mathematischen Intuitionen setzen, sondern auf unfehlbare, maschinengeprüfte Beweise.

Kurz gesagt: Banwait hat den Beweis für die Ramanujan-Nagell-Gleichung nicht nur geschrieben, sondern ihn in eine digitale Festung verwandelt, die so stark ist, dass kein Fehler mehr durchrutschen kann. Und er hat dabei gelernt, wie man mit KI zusammenarbeitet, um diese Festung schneller zu bauen.

Technische Zusammenfassung

1. Problemstellung

Das Paper adressiert die formale Verifizierung des Ramanujan–Nagell-Theorems, einer klassischen diophantischen Gleichung. Die Gleichung lautet:
$$x^2 + 7 = 2^n$$
wobei $x$ eine ganze Zahl und $n$ eine natürliche Zahl ist.
Das Theorem besagt, dass es genau fünf Paare $(n, x)$ gibt, die diese Gleichung erfüllen:
$$(n, x) \in \{(3, \pm1), (4, \pm3), (5, \pm5), (7, \pm11), (15, \pm181)\}.$$

Obwohl der Beweis seit 1948 (durch Nagell) bekannt ist und in Standardlehrbüchern der algebraischen Zahlentheorie vorkommt, fehlte bislang eine vollständige, maschinell überprüfte Formalisierung in einem Theorembeweiser. Dies ist die erste Formalisierung einer Vermutung Ramanujans und die erste vollständige Lösung einer spezifischen exponentiellen diophantischen Gleichung in einem solchen System.

2. Methodik und Architektur

Die Arbeit wurde mit dem interaktiven Theorembeweiser Lean 4 unter Verwendung der umfangreichen Bibliothek Mathlib durchgeführt. Der Beweis folgt dem klassischen Ansatz von Stewart und Tall, wird jedoch durch die Anforderungen der formalen Verifikation erheblich erweitert.

Architektur der Formalisierung:
Die Beweiskette erstreckt sich über fünf Hauptdateien (insgesamt ca. 3.570 Zeilen Code und 125 Deklarationen) und gliedert sich in zwei Schichten:

1. Algebraische Infrastruktur (3 Dateien):

   • QuadraticIntegerROI.lean & RingOfIntegers.lean: Identifikation des Rings der ganzen Zahlen $\mathcal{O}_K$ des quadratischen Zahlkörpers $K = \mathbb{Q}(\sqrt{-7})$. Da $-7 \equiv 1 \pmod 4$, ist der Ring $\mathbb{Z}[\frac{1+\sqrt{-7}}{2}]$, nicht $\mathbb{Z}[\sqrt{-7}]$.
   • FieldIsomorphism.lean: Konstruktion eines expliziten Isomorphismus zwischen der „natürlichen" Darstellung von $K$ (Generator $\sqrt{-7}$) und der Darstellung, die für die ganzzahlige Hülle geeignet ist (Generator $\frac{1+\sqrt{-7}}{2}$). Dies ist notwendig, da Mathlib diese als unterschiedliche Typen behandelt.
   • Helpers.lean: Berechnung algebraischer Invarianten: Diskriminante ($-7$), Klassenzahl ($1$, was impliziert, dass $\mathcal{O}_K$ ein Hauptidealring ist), Einheitsgruppe ($\{\pm 1\}$) und Irreduzibilität der Elemente $\theta$ und $\theta'$.

2. Der eigentliche Beweis (1 Datei):

   • Basic.lean: Umsetzung des Hauptbeweises. Dies umfasst die Faktorisierung in $\mathcal{O}_K$, die Analyse des Falls gerader und ungerader $n$, die binomische Expansion, die Reduktion modulo 42 und den Eindeutigkeitsbeweis pro Restklasse.

Schlüsseltechniken:

• Nutzung von Unique Factorization Domains (UFD) in $\mathcal{O}_K$.
• Anwendung von $p$-adischen Bewertungen (insbesondere für $p=7$) im Eindeutigkeitsbeweis.
• Verwendung von binomischen Sätzen und Kongruenzen modulo 42 zur Einschränkung der möglichen Exponenten.

3. Wichtige Beiträge

Die Arbeit leistet drei wesentliche Beiträge:

1. Maschinell überprüfter Beweis: Der erste vollständige, von einem Computer verifizierte Beweis des Ramanujan–Nagell-Theorems. Der Code enthält keine sorry-Axiome und hängt nur von den drei Standard-Axiomen von Lean ab.
2. Infrastruktur für quadratische Zahlkörper: Entwicklung einer wiederverwendbaren Bibliothek für die Arbeit mit Ringen ganzer Zahlen in quadratischen Erweiterungen von $\mathbb{Q}$. Dies beinhaltet die korrekte Identifikation der ganzzahligen Hülle, die Berechnung der Klassenzahl und die Bestimmung der Einheitsgruppe. Diese Infrastruktur ist auf andere quadratische Körper übertragbar.
3. Analyse der Lücke zwischen informellem und formalem Beweis: Eine detaillierte Untersuchung, wo Standardbeweise in Lehrbüchern erhebliche Elaboration benötigen, wenn sie formalisiert werden.

4. Ergebnisse und technische Herausforderungen

Der Beweis bestätigt die fünf bekannten Lösungen. Die Arbeit hebt jedoch mehrere signifikante Herausforderungen hervor, die in informellen Beweisen oft übersehen werden:

• Isomorphismen und Integralität: Die Verbindung zwischen verschiedenen Darstellungen desselben Zahlkörpers (z. B. $\mathbb{Q}(\sqrt{-7})$ vs. $\mathbb{Q}(\frac{1+\sqrt{-7}}{2})$) erfordert explizite Isomorphismen und den manuellen Transport von Eigenschaften wie der „integralen Hülle" (IsIntegralClosure). Dies ist in Lehrbüchern trivial, in Lean jedoch aufwendig.
• Typklassen-Infrastruktur (Typeclass Diamonds): Es traten Probleme auf, wenn ein Typ (wie der Zahlkörper) mehrere, aber propositionale gleiche Algebra-Instanzen besitzt. Diese mussten explizit aufgelöst werden, um Konflikte im Typklassensystem zu vermeiden.
• Arithmetik in $\mathcal{O}_K$: Viele einfache Umformungen, die über $\mathbb{Z}$ trivial sind (z. B. mit ring oder omega lösbar), erfordern in $\mathcal{O}_K$ komplexe Kettungen von Typumwandlungen (Casting) und manuelle Beweisschritte, da keine automatischen Entscheidungsprozeduren für diesen Ring existieren.
• Einheitsgruppenbestimmung: Der Beweis, dass die Einheitsgruppe nur $\{\pm 1\}$ ist, erforderte eine detaillierte Fallunterscheidung basierend auf der Totienten-Schranke und der Nicht-Existenz bestimmter Einheitswurzeln in $\mathbb{Q}(\sqrt{-7})$. Dies war einer der rechenintensivsten Teile.
• Binomische Expansion und Modulo-Reduktion: Die Aufteilung von Summen und die Umindizierung (Reindexing) von binomischen Reihen erforderten umfangreiche Beweise für Mengenoperationen (Finset.sum_filter, sum_bij).

5. Bedeutung und Rolle der KI

Das Paper ist ein Meilenstein für die formale Verifikation in der Zahlentheorie. Es zeigt, dass komplexe Sätze der algebraischen Zahlentheorie in modernen Beweisassistenten handhabbar sind, wenn die entsprechende Infrastruktur vorhanden ist.

Ein besonderes Merkmal dieses Projekts ist der extensive Einsatz von KI-gestützten Tools (Claude Code und Aristotle):

• Taktik-Vorschläge: KI half bei der Auswahl der richtigen Beweistaktiken für Routineaufgaben.
• Proof Repair: Bei Updates von Mathlib half die KI, API-Änderungen automatisch zu kompensieren.
• Lemma-Suche: KI beschleunigte die Suche nach passenden Lemmata in der riesigen Mathlib-Bibliothek.
• Boilerplate-Generierung: Wiederkehrende Beweisstrukturen (z. B. Fallunterscheidungen) wurden schneller generiert.

Fazit:
Die Arbeit demonstriert, dass KI-Tools die Einstiegshürde für die formale Verifikation senken können, ohne die Korrektheit der Beweise zu beeinträchtigen, da der Lean-Kernel alle Beweise final verifiziert. Sie legt einen wichtigen Grundstein für zukünftige Formalisierungen in der algebraischen Zahlentheorie und zeigt, wie theoretische Mathematik und maschinelles Lernen synergistisch zusammenwirken können.