Das US-amerikanische KI-Unternehmen Anthropic hat einen bedeutenden Durchbruch an der Schnittstelle von künstlicher Intelligenz und theoretischer Mathematik erzielt. Dem KI-Modell Claude gelang es in einem Zeitraum von nur elf Tagen, Fermats letzten Satz zu formalisieren.
Dieser Prozess überführte den komplexen menschlichen Beweis in eine maschinenlesbare Form, die anschließend durch einen Computer auf ihre logische Unversehrtheit geprüft werden konnte.
Umfangreiche Rechenleistung und Lean-Code
Die am 7. September veröffentlichte Formalisierung stellt ein Projekt von enormem Ausmaß dar. Der resultierende computergeprüfte Beweis umfasst etwa 13 Millionen Zeilen Code in der spezialisierten Programmiersprache Lean. Ein sogenannter Lean-Kernel wurde eingesetzt, um die Korrektheit des gesamten Codes sowie der logischen Ableitungen zu verifizieren.
Im Verlauf der elf Tage dauernden Berechnung erzeugte die künstliche Intelligenz insgesamt 30.300 unterstützende mathematische Aussagen. Davon bilden 29.500 Zwischen-Theoreme die finale, zusammenhängende Beweiskette. Dokumentiert wurde dieser Prozess in einem Umfang von rund sechs Milliarden Wörtern, was die enorme Tiefe der formalen Aufarbeitung verdeutlicht.
Vergleich mit menschlicher Forschungsarbeit
Branchenexperten heben insbesondere die Geschwindigkeit des Projekts hervor. Während die KI die Aufgabe in weniger als zwei Wochen bewältigte, wird die benötigte Zeit für eine rein menschliche Formalisierung desselben Beweises auf etwa zehn Jahre geschätzt. Es handelt sich bei dem Erfolg jedoch nicht um eine neue mathematische Entdeckung im eigentlichen Sinne. Vielmehr wurde der ursprüngliche Beweis von Andrew Wiles aus dem Jahr 1995 als Vorlage genutzt.
Während KI-Systeme komplexe logische Probleme lösen, müssen Unternehmen die rechtlichen Rahmenbedingungen dieser Technologie im Blick behalten. Dieser kostenlose Umsetzungsleitfaden bietet einen kompakten Überblick über alle Anforderungen, Pflichten und Fristen der neuen EU-KI-Verordnung. EU AI Act in 5 Schritten verstehen: Jetzt E-Book kostenlos herunterladen
Dieses Vorhaben war nur durch umfangreiche Vorarbeiten möglich. Mathematiker hatten in den vergangenen zwei Jahrzehnten ein notwendiges Gerüst für derartige Arbeiten geschaffen. Zudem basierte der Erfolg von Claude auf einem detaillierten menschlichen Bauplan, der den Rahmen für die KI-gestützte Überführung in Lean-Code vorgab.
Reaktionen aus der Wissenschaft und Ausblick
In der mathematischen Fachwelt löste das Ergebnis große Aufmerksamkeit aus. Die Mathematiker Alex Kontorovich, Kevin Buzzard und Daniel Litt zeigten sich von der Leistungsfähigkeit des Systems und der Präzision der Formalisierung beeindruckt. Die erfolgreiche Anwendung von KI auf eines der bekanntesten Probleme der Zahlentheorie unterstreicht das Potenzial für die Zukunft der formalen Verifikation.
Wer sich mit dem Einsatz hochmoderner KI-Systeme befasst, sollte auch die regulatorischen Kennzeichnungs- und Dokumentationspflichten kennen. Erfahren Sie in diesem kostenlosen Report, welche Systeme als Hochrisiko gelten und was Verantwortliche jetzt konkret tun müssen. Kostenlosen Report zur KI-Verordnung anfordern
Analysten deuten an, dass dieser Erfolg weitreichende Konsequenzen für die Forschung haben könnte. So wird unter anderem in Indien erwogen, verstärkt in den Bereich der formalen Verifikation zu investieren. Die Fähigkeit, komplexe logische Strukturen in kurzer Zeit maschinell abzusichern, gilt als Schlüsseltechnologie für die Entwicklung hochsicherer Software und die Validierung wissenschaftlicher Erkenntnisse.
Das Projekt, welches Anfang September angekündigt worden war, belegt die zunehmende Reife von KI-Modellen bei der Bewältigung hochgradig strukturierter und logisch anspruchsvoller Aufgaben. Die Kombination aus jahrzehntelanger mathematischer Vorarbeit und moderner Rechenkapazität hat eine neue Dimension der mathematischen Beweisführung eröffnet.
