Case study: proving sqrt(2) irrational with LPTP and an LLM

Stellen Sie sich vor, Sie sind ein Detektiv, der versucht, ein Rätsel zu lösen, das die Menschheit seit über zweitausend Jahren vor ein Rätsel stellt: Ist die Quadratwurzel aus 2 eine „rationale“ Zahl? In der Welt der Mathematik ist eine rationale Zahl wie ein perfektes Stück Kuchen, ein sauberer Schnitt (wie 3/4 oder 5/2). Eine irrationale Zahl ist eine chaotische, niemals endende Dezimalzahl, die niemals als einfacher Bruch geschrieben werden kann. Die Quadratwurzel aus 2 ist die Länge der Diagonale eines Quadrats mit Seiten der Länge 1, und antike Mathematiker haben bewiesen, dass sie „chaotisch“ ist – sie kann kein Bruch sein.

Stellen Sie sich nun vor, Sie hätten zwei sehr unterschiedliche Werkzeuge, um Ihnen bei der Lösung dieses Rätsels zu helfen. Das erste ist ein sehr strenger, roboterhafter Schiedsrichter namens LPTP. Er spricht eine sehr präzise, logische Sprache (basierend auf Prolog) und akzeptiert einen Beweis nur dann, wenn jeder einzelne Schritt mathematisch perfekt ist. Wenn Sie auch nur einen winzigen Fehler machen, schlägt er mit dem Hammer auf und sagt: „Nö, ungültig.“ Das zweite Werkzeug ist ein Large Language Model (LLM), das wie ein superintelligenter, kreativer Schüler ist, der fast alles gelesen hat, was jemals geschrieben wurde. Dieser Schüler ist gut darin, den nächsten Schritt in einer Geschichte oder einem mathematischen Problem zu erraten, aber manchmal „halluziniert“ er – er erfindet Fakten, die gut klingen, aber eigentlich falsch sind.

Die große Frage ist: Können wir diese beiden zusammenbringen? Können wir den kreativen Schüler die schwere Arbeit des Schreibens des Beweises übernehmen lassen, während der strenge Schiedsrichter jeden einzelnen Satz prüft, um sicherzustellen, dass der Schüler nicht lügt? Diese Arbeit untersucht genau diese Partnerschaft, wobei sie das uralte Rätsel der Quadratwurzel aus 2 als Testfall verwendet.

---

Das große Team-Up zur Beweisprüfung

In dieser Arbeit versuchten die Autoren zu untersuchen, ob sie eine moderne KI (speziell ein Modell namens Claude) einsetzen können, um zu beweisen, dass die Quadratwurzel aus 2 irrational ist, aber mit einem Twist: Der Beweis musste in einem sehr spezifischen, strengen Format geschrieben werden, das der roboterhaften Schiedsrichter (LP|P) verstehen und verifizieren kann. Sie wollten nicht bloß, dass die KI sagt „es ist wahr“; sie wollten, dass die KI die eigentliche schrittweise Logik schreibt, die der Schiedsrichter dann bewertet.

Die Geschichte beginnt mit einer einfachen Idee. Um zu beweisen, dass die Quadratwurzel aus 2 irrational ist, nimmt man normalerweise das Gegenteil an: dass sie ein Bruch aus zwei ganzen Zahlen, $p$ und $q$, ist, die keine gemeinsamen Teiler haben (sie sind „teilerfrem“). Wenn man die Mathematik betreibt, stößt man schließlich auf einen Widerspruch, bei dem beide Zahlen gerade sein müssen, was bedeutet, dass sie doch einen gemeinsamen Faktor haben (2). Dies bricht die Regel, dass sie teilerfrem waren, und beweist, dass die ursprüngliche Annahme falsch war.

Die Autoren versuchten, die KI dazu zu bringen, diesen Beweis in der strengen Sprache von LPTP zu schreiben. Anfangs war die KI wie ein Schüler, der zwar die Geschichte kennt, aber den Aufsatz nicht im geforderten Format schreiben kann. Sie versuchte, Schritte zu überspringen oder logische Sprünge zu machen, die der Schiedsrichter nicht akzeptieren würde.

Hier fand die Teamarbeit statt. Die Autoren richteten eine Feedbackschleife ein:

1. Die KI versucht, einen Beweisschritt zu schreiben.
2. Der Schiedsrichter (LPTP) überprüft ihn.
3. Wenn der Schiedsrichter einen Fehler findet, zeigt er exakt die Zeile auf, in der die Logik brach.
4. Die Autoren zeigen diesen Fehler der KI.
5. Die KI versucht es erneut und korrigiert den spezifischen Fehler.

Dieser Prozess war wie ein Spiel von „Heiß und Kalt“. Der Schiedsrichter sagte nicht einfach nur „falsch“; er sagte: „Du hast einen Fehler in Schritt 4 gemacht“, was es der KI ermöglichte, ihren Kurs zu korrigieren.

Die Ergebnisse: Ein Teilerfolg

Das Experiment war ein Erfolg, allerdings mit Einschränkungen. Die KI war in der Lage, viele der kleineren, leichteren Teile des Puzzles eigenständig zu beweisen. Zum Beispiel bewies sie erfolgreich, dass „wenn eine Zahl gerade ist, ihr Quadrat ebenfalls gerade ist“ oder dass „2 mal eine Zahl gerade ist“. Die Autoren nennen dies „Lemmata“ (kleine Hilfsbeweise). Die KI beherrschte diese Aufgaben korrekt und entwickelte manchmal sogar neue Hilfs-Ideen, an die die Menschen nicht gedacht hatten.

Doch für den schwierigsten Teil des Beweises – die spezifische Logik, die zeigt, warum die Quadratwurzel aus 2 kein Bruch sein kann – blieb die KI stecken. Sie konnte den richtigen Pfad nicht allein finden. Daher mussten die menschlichen Autoren eingreifen und der KI einen „Hinweis“ geben oder sogar die Hauptstruktur des Beweises selbst schreiben und die KI bitten, die kleineren Lücken zu füllen.

Am Ende produzierten sie einen vollständigen, formalen Beweis dafür, dass die Quadratwurzel aus 2 irrational ist. Dieser Beweis wurde teilweise von der KI geschrieben und vollständig vom Roboter-Schiedsrichter geprüft. Der Schiedsrichter gab ihm eine bestandene Note und bestätigte, dass die Logik fundiert war.

Was das bedeutet

Die Arbeit behauptet nicht, dass die KI nun in der Lage ist, alle mathematischen Probleme im Alleingang zu lösen. Tatsächlich zeigen die Autoren explizit auf, dass die KI dies nicht alleine schaffen kann; ohne die menschliche Anleitung und die strenge Prüfung durch den Schiedsrichter hätte die KI wahrscheinlich einen falschen oder fehlerhaften Beweis erstellt.

Stattdessen schlägt die Arbeit einen neuen Arbeitsweg vor: KI als Entwurfsautor, Menschen als Editoren und formale Werkzeuge als Faktenchecker. Die KI ist schnell und kreativ, generiert Ideen und füllt Details aus, während das formale Werkzeug (LPTP) als unermüdliches Auge fungiert, das Halluzinationen und Fehler erwischt.

Die Autoren testeten auch andere automatisierte mathematische Werkzeuge (genannt ATPs), um zu sehen, ob sie die Aufgabe schneller erledigen könnten. Diese Werkzeuge waren schnell und kostenlos, produzierten jedoch Beweise, die für Menschen schwer lesbar waren und nicht einfach in die Bibliothek verifizierter Mathematik aufgenommen werden konnten. Der KI-Ansatz hingegen, obwohl langsamer und mit menschlicher Hilfe verbunden, produzierte Beweise, die lesbar waren und sicher für die zukünftige Verwendung gespeichert werden konnten.

Kurz gesagt zeigt diese Arbeit, dass wir uns nicht zwischen menschlicher Intuition und maschineller Präzision entscheiden müssen. Indem wir die KI die schwere Arbeit des Entwerfens und die strengen Werkzeuge die Bewertung übernehmen lassen, können wir ein System aufbauen, in dem die KI uns hilft, komplexe mathematische Wahrheiten zu beweisen, solange wir einen Menschen an Bord haben, der das Steuer führt, und einen strengen Schiedsrichter, der die Karte prüft. Die Quadratwurzel aus 2 bleibt irrational, aber jetzt haben wir eine neue, kollaborative Art, dies zu beweisen.