Anthropic: Claude half bei der Formalisierung von Fermats letztem Satz in Lean

Anthropic hat neue Forschung veröffentlicht, in der Claude zur Formalisierung von Fermats letztem Satz in Lean eingesetzt wurde. Lean ist ein Beweisassistent, der mathematische Argumente Schritt für Schritt prüft. Die Meldung bedeutet nicht, dass das Modell eigenständig einen neuen Beweis gefunden hat. Wichtiger ist der praktische Punkt: KI kann helfen, stark verdichtete menschliche Beweise in maschinenprüfbaren formalen Code zu übertragen.

Fermats letzter Satz gehört zu den berühmtesten Ergebnissen der Mathematik. Andrew Wiles bewies ihn in den 1990er Jahren, doch der Beweis nutzt tiefe Werkzeuge aus Zahlentheorie und algebraischer Geometrie. Ein Resultat dieser Größe zu formalisieren ist etwas anderes, als eine erklärende Beweisskizze zu schreiben. Jede Definition, jede Abhängigkeit, jede Umformung und jeder logische Schritt muss so explizit sein, dass der Beweisassistent ihn akzeptiert. Auch für Fachleute ist das langsam und anspruchsvoll.

Anthropic beschreibt Claude als Mitarbeiter in diesem Beweis-Engineering. Das Modell kann Lean-Code vorschlagen, mathematische Aussagen in formale Syntax übersetzen, Fehler reparieren und Wege anbieten, Zwischenlemmata zu verbinden. Die Forscher müssen weiterhin entscheiden, ob ein Pfad mathematisch trägt, den generierten Code prüfen und das System lenken, wenn der Beweiszustand schwierig wird. Es geht also um nützliche Unterstützung, nicht um den Wegfall menschlicher Urteilskraft.

Formale Beweise sind ein harter Test für Sprachmodelle. Ein Modell kann überzeugend klingen und trotzdem falsch liegen, während Lean einen Beweis nicht akzeptiert, wenn die Logik nicht typprüft. Dadurch entsteht eine Feedbackschleife, in der viele Fehler automatisch sichtbar werden. Auch der Erfolgsmaßstab verändert sich. Es zählt nicht nur, ob eine KI einen schönen Beweistext schreibt, sondern ob sie verifizierbare Artefakte in einem strengen formalen System voranbringt.

Für den KI-Markt weist die Forschung auf eine reifere Nutzung in Wissenschaft und Technik. Modelle können mühsame Schleifen aus Übersetzung, Suche und Reparatur übernehmen und Expertenteams beschleunigen. Formale Mathematik, Programmverifikation und sicherheitskritische Technik brauchen mehr als flüssige Sprache. Sie benötigen auditierbare Begründungsketten und Ergebnisse, die externe Werkzeuge prüfen können. Wenn Modelle in solchen Grenzen besser werden, erhöhen sie die Produktivität, ohne die fachliche Kontrolle zu ersetzen.

Anthropic stellt die Arbeit ausdrücklich als Schritt dar, nicht als Endpunkt. Große Theorem-Formalisierungen bleiben schwierig und hängen weiter von menschlicher Planung und Korrektur ab. Trotzdem passt die Veröffentlichung zu einem größeren Muster: Frontier-KI wird zunehmend daran gemessen, ob sie in anspruchsvollen Umgebungen verifizierbare Arbeitsprodukte liefern kann.