Claude formalisiert Fermats letzten Satz in elf Tagen

Anthropic hat am 4. September 2026 laut eigener Forschungsmitteilung den ersten vollständigen, computergeprüften Beweis von Fermats letztem Satz veröffentlicht. Claude formalisierte den Beweis demnach weitgehend autonom innerhalb von elf Tagen in der Programmiersprache Lean.

Nach Angaben von Anthropic umfasst das Ergebnis 29.500 im fertigen Beweis verwendete Zwischentheoreme. SiliconANGLE berichtet außerdem von mehreren Dutzend parallel eingesetzten Agenten und rund sechs Milliarden erzeugten Tokens. Eine neue mathematische Idee folgt aus diesem Aufwand allerdings nicht.

Von 129 Seiten zu prüfbarem Code

Fermats letzter Satz besagt, dass es für Exponenten größer als zwei keine positiven ganzen Zahlen gibt, die die Gleichung aⁿ + bⁿ = cⁿ erfüllen. Andrew Wiles legte 1995 einen 129 Seiten langen Beweis vor, dessen Prüfung laut Anthropic Monate dauerte.

Eine Formalisierung übersetzt eine solche Argumentation in eine Sprache, deren einzelne Beweisschritte ein Computer kontrollieren kann. Lean dient dabei als Beweisassistent: Fehlt eine notwendige Begründung oder bricht eine Abhängigkeit, akzeptiert das System den Schritt nicht. Das ist eine engere Kontrolle als bei einer Textantwort, die lediglich schlüssig klingt.

Mehrere Dutzend Agenten, ein Beweisobjekt

SiliconANGLE berichtet von mehreren Dutzend parallel eingesetzten Agenten, die zusammen rund sechs Milliarden Tokens erzeugten. Wie genau die einzelnen Agenten ihre Teilbeweise untereinander abstimmten, geht aus den verfügbaren Berichten nicht hervor.

Die Arbeitsform macht den Unterschied. Getrennte Modellläufe liefern Beiträge zu einem gemeinsamen Artefakt, das eine formale Prüfinstanz akzeptieren muss. Fehler können dadurch nicht einfach hinter überzeugender Sprache verschwinden.

Aber das klärt nicht jede Frage.

Prüfung ersetzt Herkunft nicht

Ein erfolgreicher Lean-Check bestätigt, dass die codierten Schritte innerhalb des formalen Systems zusammenpassen. Er sagt weder, wie effizient der Weg dorthin war, noch ob das System einen neuen, für Menschen verständlichen Beweisgedanken gefunden hat. Der von Anthropic beschriebene Ressourcenaufwand spricht zunächst für erhebliche Rechen- und Sucharbeit.

Anthropic ordnet den Lauf in eine längere Entwicklung ein: Kevin Buzzard vom Imperial College London hatte 2024 eine mehrjährige Gemeinschaftsinitiative zur Formalisierung von Wiles’ Beweis angestoßen. Claude traf damit auf Werkzeuge und mathematische Vorarbeit, die über Jahre aufgebaut wurden.

Diese Ebenen müssen getrennt bleiben. Der formale Checker prüft den fertigen Beweis. Aussagen über Autonomie, Ressourcenbedarf und die Organisation der Agenten stammen dagegen aus den Projektberichten und benötigen eine eigene Bewertung.

Autonomie braucht einen harten Prüfpfad

Für Entwicklungs- und Forschungsteams liegt der praktische Wert nicht in der Zahl eingesetzter Agenten. Relevant ist das Ergebnisformat: Es muss Fehler nach festen Regeln zurückweisen können.

In der Softwareentwicklung kann diese Rolle eine Testsuite, ein Compiler oder eine strenge Typprüfung übernehmen. Bei wissenschaftlichen Berechnungen kommen reproduzierbare Auswertungen und formale Validatoren infrage. Aufgaben ohne einen solchen Prüfpfad eignen sich deutlich schlechter für weitgehend autonome Ausführung, weil sich ein plausibles Ergebnis kaum von einem korrekten unterscheiden lässt.

Die Mindestregel ist klar: Mit wachsender Autonomie muss auch die maschinelle Kontrolle des Ergebnisses stärker werden. Milliarden Tokens ersetzen keine Abnahme.

Anthropics Beweis belegt nicht, dass Claude Mathematik allgemein „gelöst“ hat. Er demonstriert die Reichweite paralleler Agentenarbeit unter einer harten Bedingung: Ein formales System prüft jeden Beweisschritt.