【AI】Claudeがフェルマーの最終定理を11日で形式化、1300万行のLeanコードで初の完全な機械検証済み証明を完成 [すらいむ★]

Claudeがフェルマーの最終定理を11日で形式化、1300万行のLeanコードで初の完全な機械検証済み証明を完成

　AI開発企業のAnthropicは2026年9月4日、AI「Claude」がフェルマーの最終定理について最初から最後までコンピューターで検証できる証明を完成させたと発表しました。
　Claudeは11日間にわたってほぼ自律的に作業し、証明支援システム「Lean 4」で約1300万行のコードを生成。
　Anthropicはフェルマーの最終定理について初の完全な機械検証済み証明だと説明しています。

　Formalizing Fermat's Last Theorem ¥ Anthropic
　https://www.anthropic.com/research/formalizing-fermats-last-theorem

（以下略、続きはソースでご確認ください）

Gigazine 2026年09月07日 15時37分
https://gigazine.net/news/20260907-claude-fermat-last-theorem-formalizing/

リーマンはよ

1つでも本当は偽である命題を正しいとすることがこっそりできれば、
それを用いて全ての数学命題についてそれを正しいとする証明ができる。
1千万行のLEANに食わせるソースコードに、間違っているがLEANがPASS
させる命題を作れれば、それを利用してなんでも証明が成功できるだろう。
一種のせキュリティホールだ。
蟻の穴から堤も崩れる（韓非子）