Claude beweist Fermats letzten Satz in 11 Tagen – komplett computergestützt

Formalizing Fermat's Last Theorem

Anthropic hat den ersten vollständig computergeprüften Beweis von Fermats letztem Satz veröffentlicht. Claude, das KI-Modell von Anthropic, arbeitete 11 Tage lang weitgehend autonom und erzeugte einen 13 Millionen Zeilen langen Lean-Beweis mit 29.500 Zwischentheoremen. Der Beweis folgt einer vereinfachten Version von Wiles' Originalbeweis und wurde von Lean verifiziert. Kevin Buzzard von der Universität Cambridge lobte die Leistung als „außergewöhnliche Autoformalisation“. Die Arbeit zeigt, dass KI große Teile der Mathematik formalisieren kann und könnte die Verifikation neuer Ergebnisse erleichtern.