💻 computer science

A formalization of the Gelfond-Schneider theorem

Dieser Artikel beschreibt die Formalisierung des Gelfond-Schneider-Theorems, das die Transzendenz von $\alpha^\beta$ für algebraische Zahlen $\alpha \neq 0,1$ und irrationale algebraische Zahlen $\beta$ beweist, im Lean-4-Beweissystem.

Ursprüngliche Autoren: Michail Karatarakis, Freek Wiedijk

Veröffentlicht 2026-03-27

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Michail Karatarakis, Freek Wiedijk

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Das große Rätsel: Warum sind manche Zahlen „magisch"?

Stell dir vor, du hast eine riesige Bibliothek mit allen möglichen Zahlen.

Algebraische Zahlen sind wie die „Bürger" dieser Bibliothek. Sie folgen festen Regeln. Du kannst sie durch einfache Rechenoperationen (Addieren, Multiplizieren, Wurzeln ziehen) aus ganzen Zahlen herstellen. Beispiele: $\sqrt{2}$ oder $1/2$ .
Transzendente Zahlen sind die „Außenseiter". Sie gehorchen keinen solchen Regeln. Sie sind so wild und komplex, dass sie sich nicht in ein einfaches mathematisches Kästchen stecken lassen. Beispiele: $\pi$ (Pi) oder $e$ .

Die Frage, die sich die Mathematiker seit Jahrhunderten stellten, war: Was passiert, wenn wir eine algebraische Zahl (außer 0 oder 1) mit einer anderen algebraischen Zahl potenzieren, die aber „irrational" (also nicht als Bruch darstellbar) ist?

Ein berühmtes Beispiel ist $2^{\sqrt{2}}$ . Ist das Ergebnis eine „Bürger-Zahl" (algebraisch) oder ein wilder „Außenseiter" (transzendent)?

Die Lösung: Der Gelfond-Schneider-Satz

In den 1930er Jahren haben zwei Mathematiker, Gelfond und Schneider, bewiesen, dass das Ergebnis in diesem Fall immer eine transzendente Zahl ist. Das ist wie ein Gesetz der Natur: Wenn du diese spezielle Kombination machst, entsteht garantiert eine „magische" Zahl, die sich nicht durch einfache Gleichungen beschreiben lässt.

Das Problem war: Der Beweis ist extrem schwierig und lang. Er ist wie ein komplexer Tanz, bei dem man viele Schritte gleichzeitig im Kopf behalten muss.

Was haben die Autoren dieser Arbeit gemacht?

Die beiden Autoren, Michail Karatarakis und Freek Wiedijk, haben diesen Beweis nicht nur auf Papier nachvollzogen, sondern ihn in einen Computer übersetzt. Sie haben den Beweis in einer Programmiersprache namens Lean 4 geschrieben.

Stell dir vor, sie haben den Beweis nicht als Geschichte erzählt, sondern als perfekten Bauplan für ein Lego-Modell erstellt. Jeder einzelne Schritt muss logisch passen. Wenn auch nur ein kleiner Stein (ein logischer Schritt) nicht genau sitzt, lehnt der Computer das ganze Modell ab. Das ist der Vorteil: Der Computer prüft, ob wirklich jeder Schritt stimmt, ohne dass sich jemand etwas „schönredet" oder Fehler übersieht.

Wie funktioniert der Beweis? (Die Metapher der „Zauberkiste")

Der Beweis im Computer ist wie ein Detektivspiel, das in drei Akten abläuft:

Der Verdächtige (Die Annahme):
Zuerst tun die Autoren so, als wäre das Ergebnis ( $2^{\sqrt{2}}$ ) keine transzendente Zahl, sondern eine normale algebraische Zahl. Sie nehmen also an, der Verdächtige sei unschuldig.
Die Falle (Die Hilfsfunktion):
Um den Verdächtigen zu überführen, bauen sie eine mathematische „Falle" – eine sogenannte Hilfsfunktion. Das ist wie ein spezielles Werkzeug, das sie so konstruieren, dass es an bestimmten Punkten genau Null wird (wie ein Magnet, der an bestimmten Stellen anzieht).
- Das Problem: Um diese Falle zu bauen, brauchen sie viele unbekannte Zahlen (Koeffizienten).
- Die Lösung (Siegel's Lemma): Hier kommt ein mathematisches Werkzeug namens „Siegel's Lemma" ins Spiel. Stell dir das wie einen Koch vor, der weiß, wie man aus einer riesigen Schüssel mit Zutaten (Zahlen) genau die richtigen kleinen Portionen auswählt, damit das Gericht (die Gleichung) perfekt schmeckt, ohne dass die Zutaten zu groß werden. Der Beweis zeigt, dass man immer solche kleinen, passenden Zahlen finden kann.
Der Showdown (Der Widerspruch):
Jetzt vergleichen die Autoren zwei Dinge über ihre „Falle":
- Seite A (Die Algebra): Wenn die Annahme stimmt (dass die Zahl normal ist), dann muss der Wert der Falle sehr groß sein (weil algebraische Zahlen nicht zu klein werden können).
- Seite B (Die Analysis): Wenn man die Falle genau betrachtet, muss der Wert extrem klein sein (nahe Null), weil die Funktion so konstruiert wurde.
Das Ergebnis: Die Zahl kann nicht gleichzeitig „sehr groß" und „extrem klein" sein. Das ist ein logischer Widerspruch!
- Fazit: Die Annahme war falsch. Der Verdächtige ist also schuldig. Die Zahl $2^{\sqrt{2}}$ ist tatsächlich transzendent.

Warum ist das wichtig?

Vertrauen: Da der Computer jeden Schritt geprüft hat, wissen wir jetzt zu 100 %, dass der Beweis fehlerfrei ist. Keine menschliche Müdigkeit, keine übersehenen Details.
Die Bibliothek (Mathlib): Die Autoren haben nicht nur den Beweis geliefert, sondern auch die ganzen Werkzeuge (wie die Definition von „Haus einer algebraischen Zahl" oder die Analyse von Funktionen), die sie dafür brauchten, in eine öffentliche Bibliothek namens Mathlib eingebracht. Das ist wie ein Werkzeugkasten, den andere Forscher jetzt nutzen können, um noch schwierigere Rätsel zu lösen.
Die Zukunft: Dieser Beweis ist ein Sprungbrett. Jetzt, wo wir wissen, wie man solche Beweise in den Computer packt, können wir noch tiefere Geheimnisse der Zahlenwelt entschlüsseln, zum Beispiel bei komplexeren Funktionen oder in der Kryptographie.

Zusammenfassung

Die Autoren haben einen der schwierigsten Beweise der Mathematik (Hilberts siebtes Problem) in eine Sprache übersetzt, die ein Computer versteht und verifiziert. Sie haben gezeigt, dass bestimmte Zahlenkombinationen ( $2^{\sqrt{2}}$ ) immer „transzendent" sind. Dabei haben sie nicht nur das Ergebnis bestätigt, sondern auch den Weg für zukünftige Entdeckungen geebnet, indem sie die Werkzeuge für andere Forscher bereitgestellt haben.

Kurz gesagt: Sie haben den Beweis in einen Computer gesteckt, damit er für immer und ewig als wahr gilt.

1. Problemstellung

Das Paper adressiert die formale Verifizierung des Gelfond-Schneider-Theorems, welches die Lösung von Hilberts siebtem Problem darstellt. Das Theorem besagt:
Wenn $\alpha$ und $\beta$ algebraische Zahlen sind, wobei $\alpha \notin \{0, 1\}$ und $\beta$ irrational ist, dann ist $\alpha^\beta$ eine transzendente Zahl.

Obwohl der Beweis 1934 unabhängig von Alexander Gelfond und Theodor Schneider erbracht wurde, fehlte bisher eine formale Verifizierung in einem Beweisassistenten. Bisherige mechanisierte Ergebnisse in der transzendenten Zahlentheorie konzentrierten sich auf klassische Beweise für spezifische Konstanten (wie $e$ und $\pi$ ) oder einfachere Sätze (wie Liouville-Zahlen), aber nicht auf die tiefgreifende analytisch-algebraische Struktur des Gelfond-Schneider-Theorems.

2. Methodik und Implementierung

Die Autoren formalisierten den Beweis im Lean 4-Beweisassistenten unter Verwendung der Bibliothek Mathlib. Der Ansatz kombiniert algebraische Zahlentheorie und komplexe Analysis.

A. Algebraische Grundlagen

Das „Haus" einer algebraischen Zahl (House): Für algebraische ganze Zahlen ist der Betrag nicht ausreichend, um die Größe zu messen, da sie in verschiedenen Einbettungen unterschiedlich groß sein können. Die Autoren definierten das „Haus" ( $|\alpha|$ $∣ α ∣$ ) als das Maximum der Beträge aller konjugierten Zahlen.
- Technische Innovation: Statt eine Definition basierend auf den Nullstellen des Minimalpolynoms zu verwenden (was zu Problemen mit der Ordnung und Abhängigkeitstypen führte), nutzten sie eine kanonische Einbettung $K \to \prod_{\sigma: K \to \mathbb{C}} \mathbb{C}$ . Dies erlaubt die Nutzung von Normen in Banach-Algebren und vereinfacht die Beweise für Dreiecksungleichungen und Multiplikativität erheblich.
Siegel's Lemma für Zahlkörper: Der Beweis erfordert die Konstruktion einer Hilfsfunktion mit kleinen Koeffizienten in einem Zahlkörper $K$ . Da das klassische Siegel's Lemma nur für $\mathbb{Z}$ gilt, formalisierten die Autoren eine Verallgemeinerung für den Ring der ganzen Zahlen $\mathcal{O}_K$ . Dies geschah durch einen „Descent"-Argument: Transformation des linearen Systems über $\mathcal{O}_K$ in ein größeres System über $\mathbb{Z}$ , Anwendung des klassischen Lemmas und anschließendes „Lifting" der Lösung zurück nach $\mathcal{O}_K$ .

B. Analytischer Kern und Hilfsfunktion

Der Beweis läuft durch Widerspruch und nutzt eine Hilfsfunktion $R(z)$ , die an bestimmten Punkten verschwindet.

Konstruktion von $R(z)$ : Eine Funktion der Form $R(x) = \sum \eta_i e^{\rho_i x}$ wird definiert, wobei die Koeffizienten $\eta_i$ durch ein homogenes lineares Gleichungssystem bestimmt werden, das durch Siegel's Lemma lösbar ist.
Das Problem der meromorphen Funktion $S(z)$ : Der klassische Beweis führt eine globale Hilfsfunktion $S(z)$ $S (z)$ ein, die Pole an den ganzen Zahlen $1, \dots, m$ $1, \dots, m$ hat. In der klassischen Analysis werden diese Pole ignoriert, da der Integrationsweg sie vermeidet. In Lean (abhängige Typentheorie) würde eine partielle (meromorphe) Definition jedoch die Komplexität der Beweise explodieren lassen (Notwendigkeit von Subtypen, Domänen-Tracking).
- Lösung: Die Autoren konstruierten $S(z)$ als totale, stückweise holomorphe Funktion. Sie „reparierten" die hebbaren Singularitäten an den Polen, indem sie lokale Taylor-Entwicklungen (analytische Faktoren) mit der rationalen Form auf dem Komplement der Pole verklebten. Dies erforderte den Nachweis der globalen Analytizität durch Übereinstimmung der lokalen und globalen Definitionen.

C. Der Widerspruch

Der Beweis vergleicht zwei Schranken für einen spezifischen Wert $\rho$ , der aus den Ableitungen von $R(z)$ abgeleitet wird:

Algebraische Untergrenze: Da $\rho$ eine von Null verschiedene algebraische Zahl ist, muss das Produkt aus $\rho$ und seinen Konjugierten (die Norm $N(\rho)$ ) mindestens 1 betragen (nach Multiplikation mit einem geeigneten Nenner). Dies führt zu einer unteren Schranke, die exponentiell in $r$ (der Ordnung des Verschwindens) wächst.
Analytische Obergrenze: Durch Anwendung der Cauchy-Integralformel auf $S(z)$ wird eine obere Schranke für $|\rho|$ hergeleitet. Diese Schranke wächst langsamer als die algebraische Untergrenze, wenn der Parameter $r$ (und damit die Größe des Gleichungssystems) groß genug gewählt wird.
Kontradiktion: Für hinreichend große $r$ widersprechen sich die Schranken, was die Annahme beweist, dass $\alpha^\beta$ algebraisch sei, falsch ist.

3. Wichtige Beiträge

Erste Formalisierung: Dies ist die erste vollständige mechanisierte Verifizierung des Gelfond-Schneider-Theorems in einem Beweisassistenten.
Erweiterung von Mathlib: Das Projekt hat signifikante Teile der Mathlib-Bibliothek erweitert, insbesondere im Bereich der algebraischen Zahlentheorie (Haus einer Zahl, Siegel's Lemma für Zahlkörper) und der komplexen Analysis (Behandlung hebbarer Singularitäten, analytische Fortsetzung).
Strukturelle Entscheidungen: Die Wahl der kanonischen Einbettung für das „Haus" und die Konstruktion totaler Funktionen statt meromorpher Funktionen demonstrieren bewährte Methoden für die Formalisierung tiefer analytischer Sätze in Lean.
Explizite Konstanten: Im Gegensatz zu klassischen Beweisen, die oft $O(\cdot)$ -Notation verwenden, wurden alle Konstanten ( $c_1$ bis $c_{15}$ ) explizit konstruiert und verfolgt, um den finalen Widerspruch rigoros zu etablieren.

4. Ergebnisse

Der Beweis des Gelfond-Schneider-Theorems wurde erfolgreich in Lean 4 formalisiert.
Als konkrete Anwendung wurde die Transzendenz der Gelfond-Schneider-Konstante $\sqrt{2}^{\sqrt{2}}$ bewiesen.
Der Code ist öffentlich verfügbar und wurde in den Mathlib-Branch integriert.

5. Bedeutung und Ausblick

Dieses Werk ist ein Meilenstein für die formale Mathematik, da es zeigt, dass komplexe Sätze der transzendenten Zahlentheorie, die tiefgreifende Wechselwirkungen zwischen Algebra und Analysis erfordern, maschinell überprüfbar sind.

Zukünftige Richtungen:

Baker's Theorem: Die Erweiterung auf lineare Formen in Logarithmen (Baker's Theorem), was noch komplexere analytische Werkzeuge erfordert.
p-adische Versionen: Ersetzung der komplexen Analysis durch p-adische Methoden (Schnirelmann-Integrale) zur Formalisierung des p-adischen Gelfond-Schneider-Theorems.
Elliptische Kurven: Übertragung des Rahmens auf Weierstraß'sche $\wp$ -Funktionen und elliptische Kurven.
Schneider-Lang-Theorem: Verallgemeinerung auf meromorphe Funktionen, die algebraischen Differentialgleichungen genügen.
Schanuel-Vermutung: Beitrag zur formalen Überprüfung der Konsequenzen dieser noch unbewiesenen Vermutung.

Zusammenfassend liefert das Paper nicht nur einen verifizierten Beweis eines historischen Problems, sondern etabliert auch eine robuste Infrastruktur für zukünftige Fortschritte in der formalen transzendenten Zahlentheorie.