Fermat's letzter Satz in Lean 4 vollständig maschinengeprüft
Fermat's Last Theorem in Lean 4
Anthropic hat einen vollständigen, maschinengeprüften Beweis von Fermats letztem Satz in Lean 4 veröffentlicht. Der Beweis folgt dem klassischen Argument von Frey, Serre, Ribet, Wiles und Taylor-Wiles und basiert auf Mathlib. Er wurde mit Lean 4.33.1 erstellt und von zwei unabhängigen Kernen verifiziert: dem Lean-Kernel selbst und nanoda, einem in Rust geschriebenen Kernel. Das Repository enthält auch eine durchsuchbare HTML-Dokumentation des Beweises. Der Beweis ist ein Forschungsartefakt und wird nicht weiter gepflegt.
Zusammen etablieren diese Prüfungen, dass die obige Aussage aus den drei Axiomen folgt, vorausgesetzt man vertraut dem Lean-Kernel (oder nanoda) und den Prüfwerkzeugen.
- black_knight
Ich frage mich, ob irgendein Teil des Lean-Codes so geformt ist, dass er zu einer der bestehenden Lean-Bibliotheken beigetragen werden könnte.
Meine Erfahrung ist, dass es viel menschlichen Input braucht, um Fable dazu zu bringen, Code zu schreiben, der gut genug für eine Formalisierungsbibliothek ist, an der andere arbeiten können. Aber da hier sicherlich auch viele Voraussetzungen formalisiert wurden, wäre es schön, wenn nicht die ganze Mühe für einen einzigen Abschlussbeweis verschwendet würde!
(Repost eines früheren Kommentars, aber ich denke, er passt hier besser)
- superposeur
Ein Großteil des Werts eines Beweises liegt in der Entwicklung mathematischer Definitionen und Zwischen-Theoreme, die benötigt werden, um dorthin zu gelangen, Grothendieck-Stil. Diese Fähigkeit scheint immer noch jenseits der KI zu liegen (zumindest habe ich nicht von fundamental neuen und nützlichen Definitionen wie "Schema" oder "Modulform" gehört, die aus dem jüngsten Schneesturm von KI-Beweisen hervorgegangen sind). ABER, ich frage mich, ob KI diese Fähigkeit auch entwickeln könnte, durch einen Prozess des effizienten Refactorings eines großen Lean-Beweises in Lean-Teile und dann der Rückinterpretation der Teile in neue, für Menschen verständliche Definitionen mit einprägsamen Namen?
- mcapodici
Was für eine Zeit, um am Leben zu sein.
https://github.com/anthropics/fermats-last-theorem/blob/main...
- chvid
Ich denke, ein interessantes Problem, vielleicht sogar interessanteres Problem, wäre der kürzeste / prägnanteste / am einfachsten zu verstehende (formal verifizierbare) Beweis.
- rawling
Diskussion auf der Startseite: https://news.ycombinator.com/item?id=49568506