13 Millionen Zeilen Code: KI verifiziert Beweis von Fermats letztem Satz
Wie belastbar ist die Formalisierung?
Der Weg zum Ergebnis
Hintergrund: Warum der Satz so lange widerstand
Bewiesen ist Fermats letzter Satz seit 1995, doch nun hat das KI-Unternehmen Anthropic nach eigenen Angaben erstmals eine vollständig computerverifizierte Fassung dieses Beweises vorgelegt. Ein Schwarm von Claude-Agenten soll sie in elf Tagen im Beweisassistenten Lean geschrieben haben: 13 Millionen Zeilen Code, 29.500 Zwischentheoreme. Die Fachwelt hatte dafür Jahre veranschlagt. Der Code liegt offen, eine unabhängige Bewertung steht weitgehend aus.
