Feasibility of Primality in Bounded Arithmetic

Die Arbeit beweist die Korrektheit des AKS-Primzahltests innerhalb der beschränkten Arithmetik $T^{count}_2$ (bzw. $VTC^0_2$), indem sie zunächst die Gültigkeit in $S^1_2 + iWPHP$ unter zwei algebraischen Axiomen zeigt und deren Beweisbarkeit in $VTC^0_2$ nachweist, während gleichzeitig neue Formalisierungen zahlentheoretischer und algebraischer Konzepte in schwachen Theorien bereitgestellt werden.

Das Wesentliche

Das große Ziel: Den AKS-Algorithmus verstehen

Stellen Sie sich vor, Sie haben einen riesigen Haufen von Zahlen. Ihre Aufgabe ist es, herauszufinden, welche davon Primzahlen sind (Zahlen, die nur durch 1 und sich selbst teilbar sind, wie 2, 3, 5, 7, 11...).

Im Jahr 2002 haben drei Wissenschaftler (Agrawal, Kayal und Saxena) einen genialen Weg gefunden, um das sehr schnell und zuverlässig zu tun. Sie nannten ihn den AKS-Algorithmus. Vorher gab es keine Methode, die garantiert schnell war und immer das richtige Ergebnis lieferte.

Die Frage, die sich die Autoren dieses Papers stellen, ist nicht: „Funktioniert der Algorithmus?" (Das wissen wir schon).
Die Frage ist vielmehr: „Wie einfach ist der Beweis dafür, dass er funktioniert?"

Die Bibliothek der Mathematik (Bounded Arithmetic)

Um diese Frage zu beantworten, betrachten die Autoren die Mathematik nicht als einen riesigen, unendlichen Ozean, sondern als eine Bibliothek mit verschiedenen Abteilungen.

1. Die große Abteilung (Peano-Arithmetik): Hier liegen alle mathematischen Wahrheiten. Man kann hier alles beweisen, aber es dauert ewig.
2. Die Ziel-Abteilung (VTC⁰₂): Das ist der Ort, an dem die Autoren ihren Beweis gerne haben möchten. Diese Abteilung ist im Vergleich zur großen Peano-Arithmetik sehr klein und beschränkt. Sie ist stark genug, um viele nützliche Rechenprozesse zu beschreiben, aber sie ist nicht unendlich mächtig.

Die Autoren wollen zeigen: Der Beweis für den AKS-Algorithmus passt in diese Ziel-Abteilung (VTC⁰₂). Das bedeutet: Die Mathematik hinter dem Testen von Primzahlen ist so strukturiert, dass sie von einem System verstanden werden kann, das weit unter der vollen mathematischen Komplexität liegt.

Der Weg zum Beweis: Ein zweistufiger Plan

Die Autoren gehen nicht einfach von einer „schweren" zu einer „leichten" Theorie. Stattdessen nutzen sie eine clevere Strategie, um zu zeigen, dass der Beweis in der Ziel-Abteilung (VTC⁰₂) möglich ist. Sie bauen das Haus in zwei Schritten:

Schritt 1: Das Fundament legen (in S¹₂ + Werkzeuge)
Zuerst nehmen sie eine Theorie namens S¹₂. Das ist ein System, das grundlegende Rechenoperationen beherrscht, aber noch nicht alles. Um den AKS-Algorithmus hier zu beweisen, brauchen sie drei spezielle „Werkzeuge" (Axiome), die in S¹₂ allein nicht automatisch gelten:

1. Das „Verallgemeinerte Fermat-Werkzeug" (GFLT): Es erlaubt uns, komplizierte Gleichungen unter bestimmten Bedingungen zu vereinfachen, ohne den Beweis zu zerstören.
2. Das „Wurzel-Zähler-Werkzeug" (RUB): Es garantiert, dass wir die Anzahl der Lösungen (Nullstellen) eines Polynoms zuverlässig zählen können, ohne den ganzen Heuhaufen durchsuchen zu müssen.
3. Ein weiteres Werkzeug (iWPHP): Ein Prinzip, das hilft, Mengen richtig zu vergleichen.

In diesem Schritt zeigen die Autoren: „Wenn wir S¹₂ mit diesen drei Werkzeugen ausstatten, können wir beweisen, dass der AKS-Algorithmus immer richtig liegt."

Schritt 2: Die Konsolidierung (in VTC⁰₂)
Jetzt kommt der entscheidende Teil. Die Autoren zeigen, dass die Ziel-Abteilung VTC⁰₂ diese drei Werkzeuge (GFLT, RUB, iWPHP) selbst beweisen kann.
Das ist wie ein Baumeister, der sagt: „Ich habe den Bauplan für das Haus (AKS) mit diesen speziellen Schrauben erstellt. Aber keine Sorge, mein Werkzeugkasten (VTC⁰₂) kann diese Schrauben selbst herstellen."
Da VTC⁰₂ die Werkzeuge besitzt, kann es auch den gesamten Beweis für den AKS-Algorithmus durchführen.

Warum ist das wichtig? (Und was bedeutet „schwach"?)

Stellen Sie sich vor, Sie bauen ein Auto.

• Der AKS-Algorithmus ist das Auto, das fährt.
• Der Beweis ist die Bauanleitung.

Früher dachte man vielleicht: „Die Bauanleitung ist so kompliziert, dass man dafür einen Supercomputer braucht, um sie zu lesen."
Diese Arbeit zeigt: Nein, die Bauanleitung ist so einfach geschrieben, dass sie von einem System verstanden werden kann, das viel weniger mächtig ist als die gesamte Mathematik.

Ein wichtiger Hinweis zur Komplexität:
Man sollte VTC⁰₂ nicht als das „einfachste System der Welt" missverstehen.

• Im Vergleich zur vollen Mathematik ist es sehr schwach.
• Aber im Vergleich zu dem, was ein Computer in „polynomieller Zeit" (also extrem schnell) tun kann, ist es immer noch ziemlich mächtig.
  VTC⁰₂ gehört zu einer Klasse, die als „Counting Hierarchy" bekannt ist. Das bedeutet, es kann mehr als nur einfache Zählungen in Echtzeit; es kann komplexere Zählvorgänge bewältigen. Es ist also nicht strikt auf das beschränkt, was ein Computer in einer einzigen schnellen Rechenoperation tut, aber es ist weit entfernt von der unendlichen Macht der klassischen Mathematik.

Das ist ein großer Sieg für die Berechenbarkeit. Es bestätigt, dass das Testen von Primzahlen nicht nur in der Praxis schnell ist, sondern dass sein mathematischer Beweis tief in einer logischen Struktur verwurzelt ist, die wir gut verstehen und kontrollieren können.

Zusammenfassung in einem Satz

Die Autoren haben bewiesen, dass der berühmteste und schnellste Test für Primzahlen (AKS) nicht nur in der Praxis funktioniert, sondern dass sein mathematischer Beweis in der Theorie VTC⁰₂ geführt werden kann – einem System, das zwar weit schwächer ist als die gesamte Mathematik, aber stark genug ist, um die komplexen Zählvorgänge des Algorithmus zu verstehen, ohne auf unendlich mächtige Theorien zurückgreifen zu müssen.

Technische Zusammenfassung

Hier ist die überarbeitete detaillierte technische Zusammenfassung des vorliegenden Papers auf Deutsch:

Titel

Feasibility of Primality in Bounded Arithmetic (Die Machbarkeit der Primzahlprüfung in der beschränkten Arithmetik)
Autoren: Raheleh Jalali und Ondřej Ježil
Veröffentlichung: Januar 2026 (Preprint)

---

1. Problemstellung

Das zentrale Ziel der Arbeit ist die Untersuchung der Beweisbarkeit der Korrektheit des AKS-Primzahltests (Agrawal-Kayal-Saxena, 2002) innerhalb schwacher Theorien der beschränkten Arithmetik (Bounded Arithmetic).

• Hintergrund: Der AKS-Algorithmus war der erste deterministische Polynomialzeit-Algorithmus zur Primzahlprüfung. Die Frage lautet: Wie "machbar" (feasible) ist ein mathematischer Beweis für die Korrektheit dieses Algorithmus?
• Theoretischer Rahmen: In der Beweis-Komplexität entspricht die Machbarkeit der Theorie $PV_1$ (die der Klasse $P$ entspricht). Stärkere Theorien wie $S^1_2$ oder $T^2$ entsprechen komplexeren Klassen.
• Das Hindernis: Ein direkter Beweis der Korrektheit in $PV_1$ ist unwahrscheinlich, da dies implizieren würde, dass die Faktorisierung ganzer Zahlen in Polynomialzeit möglich ist (was als extrem unwahrscheinlich gilt). Zudem enthält der ursprüngliche AKS-Beweis zahlentheoretische und algebraische Aussagen (z. B. über Polynome über endlichen Körpern), die in schwachen Theorien bisher nicht formalisiert waren.
• Ziel: Zu zeigen, dass die Korrektheit des AKS-Algorithmus in der Theorie $VTC^0_2$ (und äquivalent in $T^{count}_2$) bewiesen werden kann, indem gezeigt wird, dass $VTC^0_2$ alle notwendigen algebraischen Axiome liefert, die für den Beweis in $S^1_2$ erforderlich sind.

2. Methodik

Die Autoren verfolgen einen mehrstufigen Ansatz, um die Korrektheit des AKS-Algorithmus in schwachen Theorien zu etablieren:

1. Modulare Zerlegung in $S^1_2$:
   Zunächst wird gezeigt, dass die Korrektheit des AKS-Algorithmus in der Theorie $S^1_2$ bewiesen werden kann, sofern diese um zwei spezifische algebraische Axiome erweitert wird. $S^1_2$ dient hier nicht als "mittlere" Theorie, sondern als das Gerüst, das die logische Struktur des AKS-Beweises trägt, sobald die fehlenden algebraischen Bausteine bereitgestellt werden:

   • GFLT (Generalized Fermat's Little Theorem): Eine Verallgemeinerung des kleinen Satzes von Fermat für Polynome. Sie besagt, dass $(X+a)^p \equiv X^p + a \pmod{p, X^r-1}$ für eine Primzahl $p$ und ein Polynom $X^r-1$ mit logarithmisch kleinem $r$.
   • RUB (Root Upper Bound): Ein Axiom, das eine injektive Funktion einführt, die die Wurzeln eines Polynoms über einem definierten endlichen Feld auf Zahlen abbildet, die durch den Grad des Polynoms beschränkt sind. Dies ersetzt die übliche Ungleichung "Anzahl der Wurzeln $\le$ Grad" durch eine konstruktive injektive Abbildung, die in schwachen Theorien handhabbar ist.

2. Formalisierung algebraischer Strukturen in $PV_1$:
   Um die Axiome zu rechtfertigen, werden fundamentale algebraische Konzepte in der Theorie $PV_1$ formalisiert:

   • Beweis von Legendres Formel für die Primfaktorzerlegung von $n!$.
   • Existenz von zyklotomischen Erweiterungen endlicher Körper $\mathbb{Z}/p$.
   • Korrektheit des kombinatorischen Zahlensystems (Combinatorial Number System).

3. Reduktion auf $VTC^0_2$:
   Der zweite große Schritt besteht darin zu beweisen, dass die Theorie $VTC^0_2$ (eine Erweiterung von $VTC^0$ um die "Smash"-Funktion und $PV$-Symbole) die Axiome $GFLT$ und $RUB$ sowie das schwache Taubenschlag-Prinzip ($iWPHP$) beweisen kann.

   • Dies erfordert die Nachweisbarkeit der Totalität und Korrektheit von Operationen mit hochgradigen Polynomen (High Degree Polynomials), insbesondere die Division von Polynomen mittels des Kung-Sieveking-Algorithmus.
   • Es wird gezeigt, dass $VTC^0_2$ iterierte Multiplikation und Division definieren kann ($\Sigma^B_1$-definierbar).

4. Schlussfolgerung:
   Da $VTC^0_2$ die Axiome beweist, die für den Beweis in $S^1_2$ benötigt werden, folgt, dass $VTC^0_2$ die Korrektheit des AKS-Algorithmus beweist. $VTC^0_2$ ist somit die umfassende Theorie, die das gesamte Argument trägt.

3. Schlüsselbeiträge

• Erster vollständiger Beweis der AKS-Korrektheit in Bounded Arithmetic: Die Arbeit liefert den ersten formalen Beweis der Korrektheit des AKS-Algorithmus innerhalb einer Theorie, die der Komplexitätsklasse $TC^0$ (mit Smash-Funktion) entspricht.
• Neue Algebraische Axiome: Einführung und Rechtfertigung der Axiome GFLT und RUB. RUB ist besonders innovativ, da es eine injektive Indexierung von Polynomwurzeln bereitstellt, was für die Behandlung von dünn besetzten (sparse) Polynomen in schwachen Theorien essenziell ist.
• Formalisierung von Legendres Formel und Zyklotomischen Polynomen in $PV_1$: Die Autoren zeigen, dass tiefgreifende zahlentheoretische und algebraische Sätze in der sehr schwachen Theorie $PV_1$ (die Polynomialzeit-Reasoning entspricht) bewiesen werden können.
• Kung-Sieveking-Algorithmus in $VTC^0$: Nachweis der Korrektheit des Polynomdivisionsalgorithmus von Kung-Sieveking in $VTC^0_2$, was die Totalität der Polynomdivision für hochgradige Polynome sicherstellt.
• Erhaltung der ursprünglichen Struktur: Die formalisierten Beweise folgen eng der Struktur des Originalbeweises von Agrawal, Kayal und Saxena, was zeigt, dass die beschränkte Arithmetik diese fundamentalen Ergebnisse ohne massive Umstrukturierung der Argumentation erfassen kann.

4. Ergebnisse

• Hauptsatz: Die Theorie $VTC^0_2$ (und äquivalent $T^{count}_2$) beweist die Korrektheit des AKS-Algorithmus. Das heißt, die Aussage $\forall x (\text{Prime}(x) \leftrightarrow \text{AKSPrime}(x))$ ist in diesen Theorien ableitbar.
• Hierarchie der Beweise:
  1. $PV_1$ formalisiert die notwendigen algebraischen Grundlagen (Legendre, zyklotomische Polynome).
  2. $S^1_2 + iWPHP + RUB + GFLT$ beweist die Korrektheit des AKS-Algorithmus (hier fungiert $S^1_2$ als logisches Gerüst für die modulare Zerlegung).
  3. $VTC^0_2$ beweist die Axiome $RUB$, $GFLT$ sowie $iWPHP$. Da $VTC^0_2$ diese Axiome liefert, ist der Beweis in $VTC^0_2$ abgeschlossen.
• Beziehung der Theorien: $VTC^0_2$ ist bezüglich der für dieses Papier relevanten $\Sigma^B_1$-Aussagen stärker als $T^2$. Während $T^2$ allein (ohne Zählaxiome) vermutlich nicht ausreicht, da der kleine Fermatsche Satz über $T^2$ bereits das Taubenschlag-Prinzip (PHP) implizieren würde, dessen Beweisbarkeit in $T^2$ unbekannt ist, liefert $VTC^0_2$ die notwendige Zählkapazität, um die Axiome zu beweisen, die den AKS-Beweis ermöglichen.

5. Bedeutung und Ausblick

• Reverse Mathematics: Die Arbeit trägt zur "Bounded Reverse Mathematics" bei, indem sie zeigt, welche axiomatischen Stärken notwendig sind, um moderne Algorithmen der Komplexitätstheorie zu verifizieren.
• Komplexitäts-Kavität: Es ist wichtig zu betonen, dass $VTC^0_2$ der Zählhierarchie (Counting Hierarchy) entspricht, genauer gesagt $TC^0$ erweitert um polynomielle Zeitfunktionen. Obwohl $VTC^0_2$ im Vergleich zu starken Systemen der mathematischen Logik als schwach gilt, sollte es nicht als strikt "machbar" (im Sinne von Polynomialzeit-Reasoning) charakterisiert werden. Die Frage, ob das Ergebnis auf eine noch schwächere, wirklich "machbare" Theorie (wie $PV_1$ oder $S^1_2$ ohne zusätzliche Axiome) heruntergedrückt werden kann, bleibt ein offenes Problem.
• Propositionale Übersetzung: Da die Korrektheit in $VTC^0_2$ bewiesen wird, existiert ein zugehöriges propositionales Beweissystem (Quantified Sequent Calculus $G$), in dem die Tautologien, die die Korrektheit für Eingaben beliebiger Länge ausdrücken, effizient beweisbar sind.
• Offene Probleme: Die Autoren diskutieren, ob schwächere Theorien wie $T^2 + PHP$ ausreichen, um den Beweis zu führen, und untersuchen die Rolle der Funktion $(X+a)^p$ im Kontext von Beweis-Komplexitäts-Generatoren.
• Fazit: Die Arbeit demonstriert, dass die tiefen zahlentheoretischen und algebraischen Strukturen des AKS-Algorithmus in der beschränkten Arithmetik fundiert sind. Sie zeigt, dass die "Machbarkeit" des Primzahltests auf der Ebene der Beweisbarkeit in der Theorie $VTC^0_2$ gegeben ist, wobei die Grenze zur strikten Polynomialzeit-Machbarkeit weiterhin Gegenstand der Forschung bleibt.