Im September hat Anthropic die erste vollständige Formalisierung von Fermats letztem Satz veröffentlicht – Dutzende Agenten, elf Tage, rund 6 Milliarden Ausgabe-Token und 13 Millionen Zeilen Lean-Code. Dabei half Prove2Me, eine Plattform für formalisierte Mathematik, und ein Forscher gab die Richtung vor.
Am 9. November hat Anthropic nachgelegt. Ein Team aus 1.000 Agenten auf einer frühen Fassung von Claude Fable 5.2 hat denselben Beweis ohne Prove2Me und ohne Forscher reproduziert: in 28,7 Stunden, mit einem Drittel der Ausgabe-Token, und der Beweis ist ein Siebtel so lang.
Nur Git, SQL und eine Shell
Jeder Agent saß in einer eigenen Sandbox ohne Netzzugang, mit Shell, Dateieditor, Leans Werkzeugkette samt Mathlib, einem eigenen Git-Branch und Zugriff auf eine gemeinsame Postgres-Datenbank. Eine einzige geteilte Maschine war bei etwa 100 Agenten am Ende: Mehr als die Hälfte dieser Läufe musste abgebrochen oder neu gestartet werden, weil Speicher, Platte oder CPU ausgingen.
Der Prompt nannte 60 zu beweisende Aussagen, je mit einer Zeile Beschreibung, dazu einen Satz zur klassischen Beweisroute, die Definitionen und 47 bereits bewiesene Lemmata aus dem September. Die einzige vorgegebene Struktur war eine Hierarchie: ein Anführer, 999 Helfer.
Die Agenten haben sich selbst organisiert
In den ersten zehn Minuten legte der Anführer fünf Tabellen an: announce für Anweisungen an alle, assign für Zuständigkeiten, notes als offenes Brett, subtasks als Aufgabenliste zum Abholen und landed als Protokoll fertiger Arbeit. Dann teilte er die 60 Aussagen auf Mannschaften von 16 bis 17 Helfern auf und ließ jeden Helfer erst einmal die Schwierigkeit seiner Aussage einschätzen.
Diese Einschätzung war falsch, und das ist der interessanteste Befund des Versuchs. Die Helfer hielten 47 der 60 Aussagen für im Zeitbudget nicht machbar. Der Anführer legte sie beiseite, konzentrierte alle auf die verbleibenden zehn – und nach 45 Minuten schrieb er, der Durchsatz des Teams liege „far higher than the early ‘infeasible-in-budget’ verdicts assumed“. Nach etwa 70 Minuten waren alle zehn fertig, und er holte die aussortierten zurück: „there is no reason to idle“.
Übrig blieb Langlands-Tunnell, ein klassisches Ergebnis, auf dem Wiles’ Beweis aufsetzt. Der zuständige Kapitän hatte 0,7 bis 1 Million Zeilen Lean geschätzt und die Chance auf unter ein Prozent. Der Anführer schob rund 750 Helfer darauf und schrieb: „Honest odds are low.“ Das Team baute die Arbeit als Baum auf – wer ein Stück zu groß fand, hängte kleinere darunter –, bis 2.418 Aufgaben in bis zu zehn Ebenen standen. Nach 28,4 Stunden war die Aussage bewiesen.
Drei Schichten Sicherheit, und was sie gesehen haben
Jede Sandbox lief ohne Netz, mit einem Kernel ohne ladbare Module, kexec, rohen Speicherzugriff und Kernel-Probes, im Lockdown-Modus und ohne sudo. SQL-Aufrufe liefen unter einer gemeinsamen Rolle ohne Rechte, jede Anweisung mit fünf Sekunden Zeitlimit, Schreibvorgänge über 256 MiB verweigert. Ein Klassifikator prüfte jeden Werkzeugaufruf vor der Ausführung, ein Offline-Wächter sah die Aktionen danach noch einmal durch.
Über mehr als eine Million Werkzeugaufrufe hat keiner die Schwelle zum Blockieren erreicht. Beim Nachspielen gegen den neueren Wächter kam genau einer in die Nähe: eine Prüfung auf Root-Zugriff.
Was das Team nicht konnte
Anthropic schreibt es selbst hin: Agenten geben bei schweren Problemen auf und schätzen deren Schwierigkeit falsch ein. 47 von 60 Fehlurteilen am Anfang sind kein Randfehler, und ohne den Anführer, der sie zurückholte, wäre der Lauf nach 70 Minuten mit zehn Aussagen zu Ende gewesen. Getragen hat den Lauf eine Hierarchie, die eine falsche Mehrheitsmeinung überstimmen konnte: Der Anführer holte die 47 aussortierten Aussagen zurück, nachdem das Team sich am Durchsatz der ersten zehn selbst widerlegt hatte.