POINCARÉ, ZEILE FÜR ZEILE VON DER MASCHINE GEPRÜFT

Einen Beweis zu prüfen, gehört zu den anspruchsvollsten Aufgaben der Mathematik, besonders wenn sich ein Argument über mehrere Gebiete erstreckt. Da KI die Produktion von Beweisen beschleunigt, wird verlässliche Verifikation wichtiger. Beweisassistenten wie Lean 4 bieten eine Antwort: Definitionen, Aussagen und Beweise werden als Code geschrieben, und ein kleiner, vertrauenswürdiger Kern der Software, sein „Kernel“, prüft jeden Schritt. Ein Beweis, der den Kernel passiert, belegt seine Aussage; den Menschen bleibt zu prüfen, ob die Aussage wirklich das sagt, was Mathematiker meinen.

Ein knapper Beweis, eine fehlende Bibliothek

Die von Perelman bewiesene Poincaré-Vermutung besagt, dass jede geschlossene, einfach zusammenhängende dreidimensionale Mannigfaltigkeit – anschaulich ein endlicher 3D-Raum ohne Löcher, in denen sich eine Schlinge verfangen könnte – äquivalent zur dreidimensionalen Sphäre ist. Der Beweis folgt dem von Richard Hamilton begonnenen Programm des Ricci-Flusses. Perelmans drei Preprints von 2002–2003 lieferten die Schlüsselargumente in stark verdichteter Form; ausführliche Darstellungen folgten, darunter die Monografie von John Morgan und Gang Tian aus dem Jahr 2007, der dieses Projekt folgt.

Dieser Beweis stützt sich auf geometrische Analysis, die in Leans Gemeinschaftsbibliothek Mathlib weitgehend fehlte. Ein großer Teil der Grundlagen musste von Grund auf gebaut werden.

Von Mathematikern eingefrorene Meilensteine

Zhiyuan Zhang, Axel Delaval, Bin Dong, Chunlei Liu und Kollegen von der Peking-Universität und anderen Pekinger Einrichtungen begannen im Mai 2026: drei „KI-Ingenieure“ mit mathematischer Ausbildung arbeiteten an der Seite von Mathematikern. Ihr erster Ansatz – große Teile der Hintergrundtheorie zu formalisieren – war langsam, und der entstandene Code blieb hinter ihren Erwartungen zurück.

Im September 2026 fingen sie neu an. Der Beweis wurde in etwa 90 Meilensteine zerlegt, jeder eine präzise Lean-Aussage mit den nötigen Definitionen. Mathematiker prüften diese Aussagen vor oder während ihrer Formalisierung, dann wurden sie eingefroren: Die Agenten durften sie nicht ändern, und jede Korrektur ging zurück über die Mathematiker. Da niemand jede von den Agenten geschriebene Zeile lesen konnte, wurden diese Meilensteine zu den Kontrollpunkten, an denen Menschen die Mathematik prüften.

Die Agenten arbeiteten dann parallel, über interaktive Sitzungen mit Programmierwerkzeugen – hauptsächlich Codex und Claude Code – und über ein System namens Archon Horizon, das begrenzte „Missionen“ an viele Server verteilt. Ein Bot kompilierte jeden Beitrag und führte die akzeptierten zusammen. GPT-6-Astra übernahm den Großteil der Formalisierung der Aussagen und der Beweiskonstruktion; Fable-5.1 diente für unabhängige Prüfungen, die Diagnose festgefahrener Aufgaben und die Durchsicht von Aussagen.

2,8 Millionen Zeilen in etwa zwei Wochen

Nach den Monaten der Vorbereitung dauerte die eigentliche Formalisierung gut zwei Wochen. KI-Abonnements und gemietete Server kosteten etwa 25.000 Dollar. Die Entwicklung beweist sowohl die topologische als auch die glatte Version des Satzes, kompiliert vollständig und besteht eine unabhängige Prüfung gegen Zielaussagen, die allein mit Mathlib formuliert sind.

Sie ist gewaltig: etwa 3,2 Millionen Zeilen Lean, auf 2,8 Millionen gekürzt, indem nur behalten wurde, wovon der finale Satz abhängt. Nach Zählung der Autoren ist fast die Hälfte Hintergrundtheorie. Ein klassisches Resultat, das Morgan und Tian in einer einzigen Fußnote erwähnen – über glatte Strukturen auf dreidimensionalen Mannigfaltigkeiten –, beanspruchte allein etwa 650.000 Zeilen.

Was die Menschen weiterhin taten

Die Autoren ordnen die Hindernisse in drei Arten: mathematische Lücken, Umsetzungsprobleme in Lean und Koordinationsprobleme. Menschen legten den Umfang von Aussagen fest (etwa, wann ein Resultat auf drei Dimensionen beschränkt werden sollte), entdeckten fehlende Argumente – etwa einen Schritt zur lokalen Kompaktheit, den die Agenten nicht fanden – und spürten versteckte Annahmen auf. Ihre wichtigste Lehre: Die Organisation der Arbeit war ebenso wichtig wie die Fähigkeiten der Agenten. Denselben Schluss ziehen sie aus Anthropics jüngster Formalisierung des Großen Fermatschen Satzes, die ebenfalls neu beginnen musste, nachdem frühe Versuche den Überblick über den Projektstand verloren hatten.

Geprüft, aber noch nicht aufgeräumt

Die Autoren betrachten die Arbeit nicht als abgeschlossen. Der Code steckt voller Duplikate; die Beweise der Agenten folgen nicht immer dem Referenzweg; und daraus eine wiederverwendbare Bibliothek der geometrischen Analysis zu machen, ist die nächste Aufgabe. Eine unabhängige Formalisierung derselben Vermutung durch ein anderes Team wurde ebenfalls angekündigt. Ihre Hoffnung: dass eines Tages ein einzelner Mathematiker mit solchen Werkzeugen seine eigene Forschung verifizieren kann.

Interessenkonflikt. Das Team nutzte Claude Code und das Modell Fable-5.1, beide von Anthropic, neben GPT-6-Astra, das über OpenAI-Abonnements genutzt wurde und den Großteil der Arbeit erledigte. Die Arbeit vergleicht ihr Projekt außerdem mit Anthropics Formalisierung des Großen Fermatschen Satzes. Dieser Artikel wurde von Claude geschrieben.