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/

これを検証するのも大変そうだ
AIにやらすか？

余白のやつか

>>2
この言語でエラーなしで記述できるってことは、証明が正しいってことなんだろ。

次に要らなくなるのは、数学者か。

次はLeanにバグがないことを証明しないと

Al支援による形式化か
これからの大規模証明では標準的な手法になるんだろうなあ

>>9
アルファ碁に負けた棋士はスポーツとして残ってるが学者もオリンピックくらいならあるかもな

マジでやばすぎ

人間はAIの言うがまま肉体労働するしかなくなる。

1300万行あるということは、その証明を一人の人間がすべてを目で見て読むのは不可能。

少なくとも人間の証明が間違いなかったことの補強としては有益

あと気になるのは形式化困難な分野があるのかどうか

他の分野の大定理も形式化して確かめてほしい

これこそAIが本来期待されていた役割でしょ
つまり問題解決でなく人間の証明の正しさの検証

さっさとabcでやれw

四色問題の証明をAIとLeanでよろしく

リーマン予想も頼む

>>39
（1300万行の）余白がないからここでは深掘りしないでおく、とちゃんと前置きしてるが？

人類オワタな

人間の力を 機械がはるかに超えて行ったとき
人間の足の速さを 機械がはるかに超えて行ったとき
人間の飛ぶ力を 機械がはるかに超えて行ったとき

そして今人間の知性を機械がはるかに超えていきつつある感じ

行数が多いところを見ると

スパゲッティコードで理解不能なんだろう

こけおどしで誇れるものではない

Lean言語知らんやつが見当違いのレスを繰り広げるスレ

ポアンカレ予想も形式化されたらしい(470万行)

次はABC予想?