Anthropic hat den ersten vollständig maschinengeprüften Beweis von Fermats letztem Satz vorgelegt – 13 Millionen Zeilen Lean-Code, laut Anthropic in 11 Tagen. Kevin Buzzard hat den Code selbst kompiliert: Er geht durch.
Google DeepMind hat ein globales KI-Wettermodell vorgestellt, das rohe Satellitendaten direkt verarbeitet und stündlich neu rechnet. Was die Zahlen taugen — und was das im Alpenraum bedeutet.
Ein Lean-Beweis ist kein Chatbot-Claim: Die Software prüft jeden Schritt, Halluzinieren ist strukturell unmöglich. Neue Mathematik ist trotzdem keine dabei.
Anthropic hat am 4. September den ersten vollständigen, maschinell geprüften Beweis von Fermats letztem Satz veröffentlicht. Geschrieben hat ihn ein internes Claude-Modell – laut Anthropic über elf Tage weitgehend selbstständig, in rund 13 Millionen Zeilen Code. Und das Bemerkenswerte daran ist nicht die Zahl. Es ist, dass diese Behauptung überprüfbar ist, ohne dass du Anthropic ein Wort glauben musst.
Der Beweis ist in Lean geschrieben, einem sogenannten Beweisassistenten. Das ist eine Programmiersprache, in der mathematische Aussagen so formuliert werden, dass ein Computer jeden einzelnen Schritt nachrechnen kann. Lean akzeptiert keine Abkürzung, keine Bemerkung wie «der Rest folgt analog», kein Berufen auf Bekanntes. Alles muss auf drei Grundaxiome zurückgeführt werden – und wenn irgendwo ein Glied fehlt, compiliert es schlicht nicht.
Melde dich an, um den vollständigen Artikel zu lesen. Der Zugang ist kostenlos.
