Anthropic、Lean 4でフェルマーの最終定理の完全な機械検証証明を公開
Fermat's Last Theorem in Lean 4
Anthropicは、定理証明支援系Lean 4とMathlibを用いて、フェルマーの最終定理の完全な機械検証証明を完成させ、GitHubで公開しました。証明はFrey、Serre、Ribet、Wiles、Taylor-Wilesの手法に基づき、約60,475モジュール、100万以上の宣言から構成されます。Leanカーネルによる検証に加え、Rust製の独立したカーネルnanodaでも検証され、Leanの標準的な3つの公理のみに依存していることが確認されています。ソースコードはAIエージェントによって生成され、Leanが正しさを保証しています。
Together, these checks establish that the statement above follows from the three axioms, given trust in the Lean kernel (or nanoda) and the checking tools.
HNでの議論
32- black_knight
Leanのコードの一部が、既存のLeanライブラリに貢献できる形になっているかどうか気になります。私の経験では、Fableが他の人が作業できるような形式化ライブラリに十分きれいなコードを書くには、多くの人間の入力が必要です。しかし、これは確かに多くの前提条件も形式化されているので、すべての努力が一つの頂点となる証明に無駄にならないのであれば、それは素晴らしいことです。（以前のコメントの再投稿ですが、ここに置く方が適切だと思います）
- superposeur
証明の価値の多くは、そこに到達するために必要な数学の定義や中間定理の開発にあります、グロタンディーク風に。この能力はまだAIには超えられないように思えます（少なくとも、最新のAI証明の雪崩から「スキーム」や「モジュラー形式」のような根本的に新しく有用な定義が現れたという話は聞いたことがありません）。しかし、AIが大きなLean証明を効率的にLeanの部品にリファクタリングし、その部品を再び新しい、人間が理解できる、示唆に富んだ名前の定義に解釈するプロセスを通じて、このスキルも発展させられるのではないかと思いますか？
- mcapodici
なんて生きているのが素晴らしい時代なんだ。
https://github.com/anthropics/fermats-last-theorem/blob/main...
- chvid
面白い問題だと思いますが、おそらくさらに面白い問題は、最短/最も簡潔/最も理解しやすい（形式的に検証可能な）証明でしょう。
- rawling