Am 4. September 2026 sorgte Anthropic mit einer bahnbrechenden Ankündigung für Aufsehen in der akademischen Welt: Ein Verbund von KI-Agenten schloss die vollständige maschinelle Formalisierung von Fermats letztem Satz in lediglich 11 Tagen ab. Zum Vergleich: Ein Team renommierter Mathematiker am Imperial College London hatte für dasselbe Vorhaben ein Forschungsbudget von einer Million Pfund eingeworben und einen Zeitraum von vollen fünf Jahren veranschlagt.
Das mathematische Rätsel, das die Menschheit über 350 Jahre lang beschäftigt hatte, war bereits 1995 vom britischen Mathematiker Andrew Wiles gelöst worden. Das spektakuläre Aufeinandertreffen von 11 Tagen gegen fünf Jahre verschiebt daher nicht die Grenzen der mathematischen Erkenntnis an sich.
Was dieser Durchbruch jedoch grundlegend erschüttert, ist das über Jahrhunderte gewachsene Modell wissenschaftlichen Vertrauens, das auf das Urteil menschlicher Gutachter setzt. Ein wegweisender Beweis wandelte sich von „jahrelangem Peer-Review durch fehlbare Mathematiker“ zu „einer Maschine, die logische Brüche in wenigen Minuten aufdeckt“.
Ein 350 Jahre altes Rätsel offenbart die Grenzen menschlicher Gutachten
Die Geschichte des Beweises von Fermats letztem Satz liest sich wie eine Chronik des kontinuierlichen Versagens menschlicher Prüfverfahren. Als 1908 in Deutschland der Wolfskehl-Preis mit 100.000 Goldmark für einen gültigen Beweis ausgelobt wurde, gingen allein im ersten Jahr 621 vermeintlich lückenlose Ausarbeitungen ein – ausnahmslos alle enthielten fatale logische Fehler.
Das menschliche Gehirn stößt bei hochgradig verschachtelten logischen Ketten unweigerlich an kognitive Grenzen. Im Juni 1993 hielt Wiles am Isaac Newton Institute in Cambridge drei vielbeachtete Vorträge, um der Welt seinen Beweis zu präsentieren. Doch nur zwei Monate später deckte eine Routinefrage der Gutachter eine schwerwiegende Lücke im theoretischen Fundament auf.
Wiles benötigte ein weiteres zermürbendes Jahr, in dem er zeitweilig kurz vor dem Aufgeben stand, um die Lücke zu schließen. Erst im Mai 1995 konnte die endgültige, 129 Seiten lange Abhandlung veröffentlicht werden. Ein Verfahren, bei dem sich einige wenige Spitzenforscher monatelang über hunderte Seiten handschriftlicher Notizen beugen, markierte damals die absolute Belastungsgrenze menschlicher Urteilskraft.
Abbildung: Header der offiziellen Ankündigung von Anthropic. Quelle: Anthropic
13 Millionen Zeilen Maschinencode in 11 Tagen
Wie lässt sich ein dichtes Geflecht abstrakter mathematischer Symbole durch eine Maschine verifizieren? Der Schlüssel dazu heißt „Formalisierung“: die Übertragung frei formulierter, mit intuitiven Sprüngen durchsetzter Beweistexte in Maschinencode, in dem nicht das geringste Satzzeichen oder Typenattribut fehlerhaft sein darf. In der Vergangenheit galt dies als mühselige Fleißarbeit für wenige Spezialisten.
Professor Kevin Buzzard vom Imperial College London leitete ein auf fünf Jahre angelegtes Gemeinschaftsprojekt, um Fermats letzten Satz zu formalisieren. Allein die Erstellung des sogenannten Blueprint-Dokuments, das die logische Marschroute vorgab, umfasste 86 Seiten.
Anthropics Forschungsmodell Claude komprimierte diesen Fünfjahresplan auf der Prove2Me-Plattform auf weniger als zwei Wochen. Es stützte sich auf die etablierte vereinfachte Beweisführung von 1995 und generierte über 13 Millionen Zeilen Code – mehr als das Fünffache der gesamten offiziellen Mathematikbibliothek dieser Plattform.
Der Code enthält die vollständigen Beweise für 30.300 Theoreme und Hilfssätze, von denen 29.500 direkt in den finalen Beweisgraphen einflossen. Dutzende KI-Agenten arbeiteten wie unermüdliche Zahnräder parallel daran, menschliche Intuition in atomare, maschinell überprüfbare Logikketten zu zerlegen.
300.000 Dollar für absolute Gewissheit
Der Einsatz industrieller Rechenkapazitäten hat vormals immense Personalkosten in eine berechenbare Bilanz aus Rechenzeit verwandelt. Das Fünfjahresprojekt von Buzzards Team war mit einer Million Pfund veranschlagt, gebunden an Gehälter, Denkzeit und die langwierige Koordination menschlicher Wissenschaftler.
Claude benötigte für den gesamten Beweisdurchlauf hingegen rund sechs Milliarden Output-Token. Zu aktuellen Marktpreisen entspricht dies Ausgaben von etwa 300.000 US-Dollar. Den Erwerb absoluter mathematischer Gewissheit für 300.000 Dollar Rechenleistung anstelle von fünf Jahren Forschungsarbeit markiert eine unumkehrbare Neuausrichtung der ökonomischen Spielregeln in der Grundlagenforschung.
Dabei operierte das System keineswegs von Beginn an fehlerfrei. In frühen Phasen kam es zu Koordinationsproblemen zwischen den Agenten, die zum Verlust von Zwischenzuständen führten. Das System passte sich jedoch durch automatisierte Fehlerkorrekturen zügig an; fehlgeschlagene Versuche steuerten rund 7 % der nicht-trivialen Zeilen des finalen Codes bei. Die Forscher von Anthropic mussten lediglich übergeordnete Vorgaben definieren – die systematische Fehlersuche übernahm der Agentenschwarm eigenständig.
Abbildung: Beweis-DAG auf der Prove2Me-Plattform, der zeigt, wie Claude Teiltheoreme schrittweise zerlegt. Quelle: Anthropic
Das Fundament wissenschaftlichen Vertrauens geht an den Compiler über
Professor Kevin Buzzard überprüfte den millionenzeiligen Codebestand persönlich; der Compiler akzeptierte den gesamten Beweis ohne Beanstandung. Automatisierte Vergleichswerkzeuge bestätigten zudem, dass alle Theoremaussagen exakt mit bestehenden mathematischen Formalbibliotheken harmonieren. Damit gilt auch die 20 Jahre alte Benchmark-Liste der „100 formalen mathematischen Herausforderungen“ als offiziell abgeschlossen.
Wie Buzzard betonte, wurde damit kein neuer mathematischer Satz entdeckt, doch für das Gebiet der automatisierten Formalisierung liefert das Projekt einen überragenden empirischen Beweis. Wenn ein 129 Seiten langer mathematischer Beweis wie gewöhnlicher Quelltext in der Softwareentwicklung kompiliert werden kann, wandelt sich das akademische Vertrauensgefüge von Grund auf.
Bislang basierte die Anerkennung eines Beweises auf dem Renommee und der Signatur führender Koryphäen. Diese zentralisierte Autorität weicht einer neuen Gewissheit: Solange der Code sauber durch den Compiler läuft, bedarf die Wahrheit keiner menschlichen Bürgen mehr. Der Compiler hat die Rolle der letzten Verteidigungslinie übernommen.
Weiterführende Links:
- Anthropic Research
- HN-Diskussion
