Claude formalisiert Fermat-Beweis in 11 Tagen

Am 4. September veröffentlichte Anthropic einen Meilenstein der KI-Forschung: Das Modell Claude hat in elf Tagen den ersten vollständigen formalisierten Beweis des Satzes von Fermat in der Beweishilfe Lean erbracht. Das Projekt geht auf Initiative von Tianyi Peng, einem Absolventen der renommierten Yao-Klasse der Universität Tsinghua, zurück und demonstriert erstmals die Fähigkeit künstlicher Intelligenz, hochkomplexe mathematische Formalisierungen im industriellen Maßstab durchzuführen. Die Entwicklung basiert auf einem Multi-Agenten-System, das über die Plattform Prove2Me koordiniert wird. Dabei arbeiten mehrere Claude-Instanzen parallel zusammen und generieren insgesamt rund 13 Millionen Zeilen Lean-Code. Für die finale Demonstration wurden etwa 30.300 Zwischenbeweise etabliert, wovon rund 29.500 in den Kernbeweis einfließen. Der Prozess verschlang etwa sechs Milliarden Output-Tokens und folgte der historischen Beweisroute von Andrew Wiles und Richard Taylor, die elliptische Kurven, Modulare Formen und Galois-Darstellungen verknüpft. Zur Bewältigung der Komplexität trennte Prove2Me strikt zwischen mathematischen Aussagen und deren Beweisen, wodurch Abhängigkeitsgraphen verwaltet und parallele Arbeitsströme ermöglicht wurden. Die Validierung der KI-generierten Arbeit unterzog sich strengsten Prüfkriterien. Zunächst bestätigte der Mathematiker Kevin Buzzard von der Imperial College London die Funktionsfähigkeit des Codes. Systematisch wurden unvollständige Beweisschritte mit dem Lean-Platzhalter sorry vermieden; die finale Abhängigkeitskette ruht ausschließlich auf drei grundlegenden mathematischen Axiomen des Typsystems. Zur unabhängigen Verifikation wurde die gesamte Umgebung in ein externes, in Rust geschriebenes Prüfprogramm namens nanoda exportiert. Dieses validierte über 1,05 Millionen deklarierte Aussagen und bestätigte die logische Konsistenz ohne Eingriffe in die Typenprüfungsregeln. Ein spezialisierter Comparator sicherte zudem die inhaltliche Übereinstimmung mit der Originalaussage des Satzes von Fermat. Trotz des technischen Erfolgs bleibt die praktische Nutzbarkeit für die mathematische Community herausfordernd. Der generierte Code übertrifft das etablierte Mathlib-Repository um das Fünffache und weist eine für menschliche Rezensenten kaum nachvollziehbare Struktur auf. Die Trennung von maschineller Verifizierbarkeit und menschlicher Lesbarkeit bleibt ein zentrales Forschungsfeld. Rechenintern zeigten sich ebenfalls erhebliche Anforderungen: Ein vollständiger Build nutzte 96 parallele Tasks bei bis zu 153 GB Arbeitsspeicher, die separate Verifikation beanspruchte etwa 230 GB. Anthropic gab keine Gesamtkosten an, betonte jedoch den Nachweis, dass KI-Systeme heute in der Lage sind, jahrzehntealte mathematische Probleme in wenigen Tagen durch hochparallelisierte, formal verifizierte Pipelines zu durchlaufen. Die Initiative markiert einen Paradigmenwechsel hin zu maschinengestützter Mathematik, stellt jedoch gleichzeitig die Notwendigkeit künftiger Optimierungen für Code-Komprimierung und Standardisierung heraus.