💻 computer science

Auto formalisation of Chaitin and of the surprise incompleteness Theorem

Diese Arbeit präsentiert eine Fallstudie unter Verwendung eines LLMs (Claude), um Chaitins Beweis des ersten Unvollständigkeitstheorems sowie die Kritchman-Raz-Version des zweiten Unvollständigkeitstheorems (Überraschungsexamens-Paradoxon) in Agda zu autoformalisieren, wobei die Fähigkeit des Modells demonstriert wird, komplexe computergestützte Simulationen zu konstruieren und maschinell geprüfte Beweise zu erzeugen, während gleichzeitig aktuelle Stärken und Grenzen im mathematischen Schließen hervorgehoben werden.

Ursprüngliche Autoren: Thierry Coquand

Veröffentlicht 2026-06-12

📖 6 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Thierry Coquand

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 Ganze: Einem Roboter das Rechnen beibringen

Stellen Sie sich vor, Sie haben einen sehr intelligenten Roboter (eine KI namens Claude) und ein sehr strenges, regelgebundenes Mathematik-Lehrbuch namens „Basic Recursive Arithmetic“. Dieses Lehrbuch ist wie ein Spiel mit sehr spezifischen Regeln: Sie dürfen nur einfaches Zählen und einfache Logik verwenden, keine ausgefallenen Abkürzungen oder „magischen“ Tricks.

Das Ziel dieser Arbeit ist es zu sehen, ob der Roboter in der Lage ist, einen komplexen, berühmten mathematischen Beweis (darüber, warum die Mathematik Grenzen hat) zu lesen und ihn vollständig in die strikte Sprache dieses Lehrbuchs umzuschreiben, ohne dass ein Mensch eine einzige Zeile Code schreibt.

Die Antwort lautet: Ja. Der Roboter hat es erfolgreich geschafft, zwei tiefe mathematische Ideen in diese strikte Sprache zu übersetzen und einen Beweis zu erstellen, den ein Computer zu 100 % auf Korrektheit prüfen kann.

Die zwei Hauptideen

Die Arbeit konzentriert sich auf zwei berühmte Konzepte: Chaitins Beweis (im Zusammenhang mit dem ersten Unvollständigkeitssatz) und das Überraschungsexamen-Paradoxon (eine Version des zweiten Unvollständigkeitssatzes).

1. Das „Kurze Beschreibung“-Spiel (Chaitins Beweis)

Stellen Sie sich vor, Sie haben eine Bibliothek mit jeder möglichen Geschichte, die Sie mit einem begrenzten Satz an Buchstaben schreiben könnten.

Die Regel: Einige Geschichten sind sehr kurz und einfach zu beschreiben. Andere sind so komplex, dass der kürzeste Weg, sie zu beschreiben, darin besteht, die ganze Geschichte einfach auszuschreiben.
Das Problem: Chaitins Beweis versucht zu zeigen, dass es eine Geschichte gibt, die so komplex ist, dass sie nicht durch ein kurzes Programm beschrieben werden kann.
Die Herausforderung für den Roboter: Um dies zu beweisen, musste der Roboter innerhalb des Mathematik-Lehrbuchs eine „Maschine“ bauen, die eine Geschichte lesen, sie ausführen und sehen kann, was sie tut.
Die Hürde: Das Mathematik-Lehrbuch ist zu einfach, um von Natur aus „ein Programm auszuführen“, da dies normalerweise eine komplexe Funktion (wie die Ackermann-Funktion) erfordert, die das Lehrbuch nicht zulässt.
Die Lösung: Der menschliche Autor schlug einen Trick vor, den „Gandy/Howard Majorisation“ nennt. Stellen Sie sich das wie das Geben eines Tankfüllers an den Roboter vor. Anstatt die Maschine zu verlangen, ewig weiterzulaufen, berechnet der Roboter genau, wie viel „Treibstoff“ (Schritte) ein Programm benötigt, um fertig zu werden. Er baut eine spezielle „Treibstoffanzeige“, die garantiert, dass das Programm stoppt, bevor der Tank leer ist.
Das Ergebnis: Der Roboter hat diese Treibstoffanzeige eigenständig gebaut. Er hat bewiesen, dass man, wenn man versucht, eine Zahl zu beschreiben, die „zu komplex ist, um einfach beschrieben zu werden“, zu einem logischen Widerspruch führt (wie etwa dem Beweis, dass 0 gleich 1 ist).

2. Das „Überraschungsexamen“ und der Haufen Sand

Der zweite Teil der Arbeit befasst sich mit einem berühmten Paradoxon: Ein Lehrer kündigt an, dass nächste Woche eine Überraschungsprüfung stattfinden wird. Die Schüler folgern daraus, dass es nicht der Freitag sein kann (denn wenn bis Donnerstag noch keine Prüfung war, wüssten sie am Freitag, dass es der Freitag ist), also kann es auch nicht der Donnerstag sein, und so weiter... bis sie zu dem Schluss kommen, dass es gar keine Prüfung geben kann. Doch dann gibt der Lehrer sie am Mittwoch, und sie ist eine Überraschung.

Die Arbeit verwendet eine Version dieser Logik (von Kripke und Raz), um zu beweisen, dass ein mathematisches System seine eigene Konsistenz (dass es keine Widersprüche enthält) nicht beweisen kann.

Der alte Weg: Frühere Beweise zählten die Anzahl der Tage oder Zahlen, um einen Widerspruch zu finden.
Der neue Weg (Das Sorites-Paradoxon / Der Haufen Sand): Die Autoren vergleichen dies mit dem Haufen-Sand-Paradoxon.
- Wenn man einen Haufen Sand hat und ein Korn entfernt, ist es immer noch ein Haufen.
- Entfernt man ein weiteres, ist es immer noch ein Haufen.
- Wenn man immer weiter Körner entfernt, landet man schließlich bei null Körnern. Aber an welchem exakten Punkt hörte es auf, ein „Haufen“ zu sein?
Die Anwendung:
- Stellen Sie sich eine Liste von Zahlen von 0 bis zu einer riesigen Zahl $N$ vor.
- Die Logik versucht zu beweisen: „Es ist unmöglich, dass alle diese Zahlen eine kurze Beschreibung haben.“
- Der Roboter beweist dies Schritt für Schritt. Er sagt: „Wenn wir annehmen, dass die Zahlen 0 bis $N$ alle kurze Beschreibungen haben, ergibt das einen Widerspruch.“
- Dann entfernt er die 0. „Okay, wenn die Zahlen 1 bis $N$ kurze Beschreibungen haben, ergibt das immer noch einen Widerspruch.“
- Er entfernt immer eine Zahl nach der anderen (wie das Wegnehmen von Sandkörnern).
- Schließlich erreicht er einen Punkt, an dem die Liste leer ist, aber die Logik erzwingt trotzdem einen Widerspruch.
Der Clou: Die Arbeit argumentt, dass dies kein „Teufelskreis“ der Selbstbezüglichkeit ist; es ist eher wie der Sandhaufen. Man kann ein Korn (eine Zahl) sicher wegnehmen, aber wenn man es fortlaufend tut, bricht die gesamte Struktur zusammen. Dieser Zusammenbruch beweist, dass das mathematische System nicht beweisen kann, dass es sicher (konsistent) ist, ohne sich selbst zu zerstören.

Warum das wichtig ist (laut der Arbeit)

KI als Mathematik-Assistent: Die Arbeit zeigt, dass heutige KIs (wie Claude) gut genug sind, um die winzigen, mühsamen Details komplexer mathematischer Beweise zu bewältigen. Die KI kann Parser bauen, Maschinen evaluieren und logische Schritte handhaben, die Menschen normalerweise manuell durchführen müssen.
Konstruktive Mathematik: Die Arbeit hebt hervor, dass in der „konstruktiven Mathematik“ (wo man das, worüber man spricht, tatsächlich bauen muss) die Idee einer „partiellen Funktion“ (ein Programm, das vielleicht ewig läuft) schwierig ist. Der Roboter musste ein „schleifendes“ Programm verwenden, das vielleicht ewig läuft, aber der Beweis garantiert, dass es stoppt. Dies ist ein subtiler, aber entscheidender Unterschied, den die KI korrekt gehandhabt hat.
Keine magischen Tricks: Der Roboter hat keine „Taktiken“ (Abkürzungen) oder ausgefallenen Bibliotheken verwendet. Er hat alles von Grund auf neu aufgebaut, indem er nur die Basalregeln des mathematischen Systems nutzte. Dies macht den Beweis sehr robust und leicht maschinell überprüfbar.

Das Fazit

Die Arbeit ist eine Fallstudie, die zeigt, dass KI nun in der Lage ist, ein mächtiger Partner in der formalen Mathematik zu sein. Sie kann eine hochgradig abstrakte Idee (wie „Mathematik hat Grenzen“) nehmen und sie in ein starres, maschinenprüfbares Format übersetzen.

Die Autoren merken an, dass die KI zwar einen Menschen braucht, der sie leitet (wie beim Vorschlagen des „Treibstofftank“-Tricks), die KI dann aber in der Lage ist, den Code autonom zu schreiben, die Logik aufzubauen und den gesamten Prozess zu dokumentieren. Das Ergebnis ist ein vollständig verifizierter Beweis, der genau klärt, wie diese tiefen logischen Paradoxien funktionieren, indem er jegliche Mehrdeutigkeit entfernt und nur die harten, logischen Fakten hinterlässt.

Technischer Überblick: Automatische Formalisierung von Chaitin und dem Überraschungsinkomplettheitssatz

Problem und Kontext
Dieser Bericht erweitert ein vorangegangenes Experiment zur Auto-Formalisierung des zweiten Gödelschen Unvollständigkeitssatzes unter Verwendung des Large Language Models (LLM) Claude und des Beweisassistenten Agda. Das primäre Ziel ist es, die Fähigkeiten und Grenzen aktueller LLMs bei der Formalisierung komplexer mathematischer Beweise zu untersuchen, insbesondere solcher, die die interne Repräsentation von Berechnungen beinhalten. Die Arbeit konzentriert sich auf zwei spezifische Ziele: Chaitins Beweis des ersten Unvollständigkeitssatzes und die Version des zweiten Unvollständigkeitssatzes nach dem „Überraschungsprüfungsparadoxon“ von Kritchman und Raz.

Eine zentrale technische Herausforderung ist die Kodierung von Berechnung innerhalb der Basic Recursive Arithmetic (BRA), einem System (formuliert von Guard), dem es an Objekt-Quantoren und Standard-Taktiken mangelt. In einem solchen System ist die Definition einer internen Evaluationsfunktion unmöglich, da diese die primitiv-rekursiven Schranken überschreiten würde (ähnlich der Ackermann-Funktion). Das Problem erfordert die Repräsentation von Programmen und deren Ausführungsschritten vollständig innerhalb der Objektsprache, ohne sich auf Meta-Ebene-Funktionen oder externe Bibliotheken zu verlassen.

Methodik
Das Projekt verfolgt einen „spartanischen“ Ansatz, bei dem kein einziger Zeile Agda-Code vom menschlichen Autor geschrieben wurde; die Formalisierung wurde autonom von Claude auf Basis hochgradig abstrakter mathematischer Beschreibungen generiert. Die Methodologie stützt sich auf die folgenden technischen Strategien:

Ternäre String-Kodierung: Programme werden als natürliche Zahlen dargestellt, die als ternäre Strings (Ziffern 1, 2, 3) interpretiert werden. Dies ermöglicht es, die Menge der Programme der Länge höchstens $L^*$ als ein einfaches Anfangssegment der natürlichen Zahlen $\{p < N\}$ zu behandeln, wobei $N = 3^{L^*+1}$ , wodurch komplexe Enumerationsmechanismen vermieden werden.
CK-Maschinen-Implementierung: Um die Notwendigkeit einer globalen Evaluationsfunktion zu umgehen, konstruierte Claude autonom eine Kontinuations-Stack-Small-Step-Evaluationsmaschine (eine Landin CK-Maschine). Diese Maschine zerlegt Ausdrücke und verwaltet einen Stack von Kontinuationen, was es ermöglicht, die Berechnung Schritt für Schritt zu simulieren.
Gandy/Howard-Majorisierung: Eine entscheidende Hürde war der Beweis, dass die Maschine innerhalb einer bestimmten Anzahl von Schritten für eine gegebene Funktion $f$ innerhalb der Logik terminiert. Da die Schrittanzahl keine Meta-Ebene-Natürliche Zahl sein kann, leiteten die Autoren Claude dazu an, die Gandy/Howard-Majorisierungsmethode anzuwenden. Dies beinhaltet die Definition eines geschlossenen Kombinator fuel(f) mittels Primitivrekursion, der die tatsächliche Laufzeit von $f$ nachweislich majorisiert. Dies ermöglicht es, die Vollständigkeit des Interpreters intern innerhalb der BRA zu formulieren und zu beweisen.
Überraschungsprüfung als Sorites: Der Beweis des zweiten Unvollständigkeitssatzes vermeidet die Zählargumente, die von Kritchman und Raz verwendet werden. Stattdessen modelliert er das Argument als Sorites-Paradoxon (Haufen-Paradoxon). Er verläuft über eine externe Induktion auf eine Stufe $r$ und beweist, dass es unmöglich ist, dass alle Zahlen im Intervall $[r, N]$ kurze Beschreibungen haben.

Wesentliche Beiträge und Ergebnisse
Die Arbeit präsentiert einen vollständig maschinengeprüften Beweis in Agda für die folgenden Resultate für Churchs Basic Recursive Arithmetic:

Auto-formalisierter Chaitins Theorem: Das System konnte Chaitins Beweis erfolgreich formalisieren, der den Lügnersatz durch Kolmogorov-Komplexität ersetzt. Die Formalisierung erzeugt einen expliziten Beweistransformator $G$ . Der Satz besagt, dass, wenn ein Term $w$ einen Beweis der Inkompressibilität $K(out(w)) > L^*$ kodiert, dann $G \cdot w$ einen Beweis von $0=1$ kodiert. Dies wird als positive Objekthebene-Implikation formuliert, statt als metatheoretische Negation der Beweisbarkeit.
Internalisierter Zweiter Unvollständigkeitssatz: Die Arbeit formalisiert das Argument von Kritchman und Raz, um zu zeigen, dass, falls $T$ seine eigene Konsistenz ( $Con_T$ ) beweist, dann $T$ inkonsistent ( $0=1$ ) ist. Der Beweis erfolgt durch einen Abstieg von $S(0)$ (dem Prinzip des Schubfachs) zu $S(N+1)$ (einem Widerspruch), wobei jeder Schritt $S(r) \to S(r+1)$ die Konsistenzhypothese genau einmal konsumiert.
Konstruktive Erkenntnisse: Die Formalisierung hebt die Rolle partieller Funktionen in der konstruktiven Mathematik hervor. Insbesondere enumeriert das diagonale Programm ableitbare Formeln, bis ein Ziel gefunden wird. Während das Programm extern als terminierend bewiesen wird, wird seine Größe berechnet, ohne den Terminierungsbeweis zu internalisieren. Dies demonstriert eine Manifestation des Blumschen Speed-up-Phänomens, bei dem die Zulassung eines partiellen rekursiven Programms (das extern total gehalten wird) im Vergleich zu Programmen, die Halten intern zertifizieren müssen, unendlich kürzere Programme ermöglicht.

Bedeutung und Behauptungen
Die Arbeit behauptet, dass aktuelle Codierungs-LLMs wie Claude effektive Werkzeuge sind, um die granularen Details mathematischer Arbeiten zu verstehen, sofern sie unter ständiger Aufsicht operieren. Das Projekt dient als Fallstudie, die zeigt, dass:

LLMs in der Lage sind, autonom komplexe syntaktische Mechanismen (Parser, Evaluationsmaschinen) und logische Argumente (Majorisierung) zu generieren, wenn sie durch hochgradig strukturelle Hinweise geleitet werden.
Typentheorie (speziell Agda ohne Taktiken) hervorragend geeignet ist, um konkrete Mathematik mit Fokus auf Berechnung und Kodierung auszudrücken, da Beweise direkt dargestellt werden können, ohne dass Funktionsextensionalität oder Quotiententypen benötigt werden.
Das „Überraschungs“-Argument, wenn es formalisiert wird, stimmt eher mit dem Sorites-Paradoxon als mit dem traditionellen Überraschungsprüfungsparadoxon überein, da der Widerspruch aus der Iteration korrekter Schritte resultiert und nicht aus einer einzelnen selbstreferenziellen Schleife.

Die Autoren kommen zu dem Schluss, dass die Sprache der Typentheorie perfekt für diese kombinatorische, computergestützte Mathematik ist, eine zentrale Forschungsfrage jedoch bleibt: Wie gestaltet man formale Systeme, die in der Lage sind, nicht-kombinatorische Objekte mit ähnlicher Automatisierung zu handhaben. Die Formalisierung klärt implizite Details der Originalpräsentationen von Chaitin und Kritchman-Raz und bietet ein rigoroses, maschinell verifiziertes Fundament für diese Argumente innerhalb eines minimalen arithmetischen Rahmens.