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.
Anthropic liess ein internes Claude-Forschungsmodell rund 64 Stunden weitgehend autonom Minibinder-Proteine gegen fünf Skorpion-Neurotoxine entwerfen. Von 211 im Labor getesteten Designs erfüllten 17 die Binder-Kriterien, die stärksten erreichen einstellige nanomolare Affinität. Ein Gegengift ist das nicht: Getestet wurde nur die Bindung an rekombinante Toxine.
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.
