Fermats letzter Satz — die Aussage, dass die Gleichung xⁿ + yⁿ = zⁿ für ganzzahlige Exponenten n größer als 2 keine ganzzahligen Lösungen besitzt — widerstand den Mathematikern mehr als 350 Jahre lang, nachdem Pierre de Fermat um 1640 seine berühmte Randnotiz vom „zu schmalen Rand“ hinterlassen hatte. Andrew Wiles bewies den Satz Mitte der 1990er-Jahre. Nun erklärt Anthropic, ein Schwarm seiner Claude-Agenten habe geleistet, was keinem menschlichen Team zuvor gelungen war: die Übersetzung dieses Beweises in eine Form, die ein Computer Schritt für Schritt nachprüfen kann.
Nach Unternehmensangaben erzeugten dutzende weitgehend autonom arbeitende Claude-Agenten die erste vollständige, computergeprüfte Formalisierung von Fermats letztem Satz im Beweisassistenten Lean — rund 13 Millionen Zeilen Lean-Code mit etwa 29.500 Zwischentheoremen. Die Arbeit dauerte elf Tage. Der Anthropic-Forscher Tianyi Peng, dessen Gruppe an der Columbia University Werkzeuge für KI-gestützte Formalisierung entwickelt, steuerte gelegentliche High-Level-Anweisungen bei; den Rest erledigten die Agenten.
Lean ist zugleich Programmiersprache und Verifikationssystem: Mathematische Aussagen und ihre Herleitungen werden als Code notiert, den Lean gegen ein festes Regelwerk prüft. Fehlt ein Glied in der Kette, kompiliert der Beweis schlicht nicht. Genau darum geht es — das Vertrauen verlagert sich von der Sorgfalt menschlicher Gutachter auf einen kleinen, überprüfbaren logischen Kern.
Mehrere frühe Anläufe scheiterten, so das Unternehmen: Die ersten Agenten-Teams erzielten Teilerfolge, verloren aber den Überblick über den Projektzustand und arbeiteten nicht mehr effektiv zusammen. Der Durchbruch kam erst mit dem Wechsel auf Prove2Me, eine offene Plattform zur Formalisierung von Mathematik, die Peng und Kollegen an der Columbia University entwickelt haben. Sie pflegt einen gerichteten azyklischen Graphen von Theoremaussagen, anhand dessen die Agenten entscheiden, welche Beweise sie als Nächstes angehen — ein Design gegen Speicherdegradation, das zugleich Parallelarbeit ermöglicht.
Der Aufwand ist enorm: Rund sechs Milliarden Output-Token verbrauchte das Agententeam laut Anthropic; außenstehende Beobachter rechnen daraus Kosten zwischen 100.000 und 300.000 US-Dollar hoch. Dass es weitaus kleiner geht, deutet ein Nebenexperiment an: Mit drei privaten Claude-Max-Abos formalisierten Agenten den Drei-Primzahlen-Satz von Winogradow in drei Tagen.
Formalisiert wurde eine vereinfachte Fassung des Wiles-Beweises nach Darmon, Diamond und Taylor; der Code liegt samt schriftlichem Walkthrough offen im GitHub-Repository von Anthropic. Kevin Buzzard, der am Imperial College London ein Gemeinschaftsprojekt zur Formalisierung von Fermats letztem Satz leitet (seit 2024, gefördert bis September 2029), hat die Arbeit geprüft: Er kompilierte den Code selbst und ließ den Vergleichs-Komparator laufen — er hält stand. In seinem Blog Xena Project spricht Buzzard von einem großen Schritt zur automatischen Formalisierung der modernen mathematischen Literatur, betont aber, dass die Arbeit mathematisch nichts Neues biete, da sie der frühen Literatur zum Beweis folge.
Der Erfolg reiht sich in eine gemischte KI-Bilanz ein: 2024 erreichten DeepMinds AlphaProof und AlphaGeometry 2 Silbermedaillenniveau bei der Internationalen Mathematik-Olympiade. Im April 2026 löste ein 23-Jähriger mit einem einzigen Prompt an GPT-5.4 Pro ein 60 Jahre altes Erdős-Problem — der Beweis wurde später in Lean formal verifiziert. Kurz darauf widerlegte ein internes OpenAI-Modell eine 80 Jahre alte Vermutung zum Planar-Unit-Distance-Problem, wobei prüfende Mathematiker anmerkten, dass sich die Argumentation im Nachhinein teils anderen Autoren zuschreiben lässt.
Für die formale Mathematik ist die Botschaft, dass Infrastruktur so wichtig sein kann wie rohe Modellstärke: Entscheidend scheint der Planungsgraph von Prove2Me gewesen zu sein, nicht ein klügeres Modell. Für das Feld insgesamt verschiebt sich mit einem maschinell geprüften Beweis eines berühmten Satzes in unter zwei Wochen — zu Kosten in der Größenordnung einer kleinen Förderung — der Maßstab, was „einen Beweis verifizieren“ bedeutet und wie viel der mathematischen Literatur künftig auf computergeprüftem Fundament stehen könnte.
