注目★★★★★Hacker News
Fermatの最終定理、Lean 4.33.1で完全機械検証
30秒で把握
- 1AnthropicがFermatの最終定理をLean 4.33.1で完全検証
- 2標準3公理のみ使用し60,475モジュールをLeanカーネルが検査
- 3comparatorとnanoda 0.4.13が同一環境を独立検証
要約
Anthropicは、Fermatの最終定理をLean 4.33.1とMathlibで完全に機械検証した研究成果を公開した。Leanの標準3公理だけに依存し、sorry・追加公理・native_decideを使わず、60,475モジュールをカーネルが検査した。leanprover/comparatorによる再検証に加え、Rust製の独立カーネルnanoda 0.4.13も同じ環境の1,052,234宣言をエラーなく検査した。証明経路と29,511定理、1,450定義モジュールを含む約390MBのHTML資料をオフラインで閲覧できる。研究用成果物で、保守やコントリビューション受付は行わない。
あなたへの影響
Leanで定理証明を検証したい日本のエンジニアは、Lean 4.33.1とMathlibの固定バージョンをそろえ、まずビルドとcomparatorの再実行を検討するとよい。
推奨：証明の各中間定理が数学的意味を正しく表すかは、最終的に読者が確認する必要がある。