【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/

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

機械検証済み証明を完成・・・日本語がワカラン

余白のやつか

>>2
AIにやらせたヤツらが当然自分たちで証明だよ

>>2
オマエはこの証明がどんなものか解ってないな

GTP6のインパクトがすごいからIPO前に頑張ってるな

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

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

人類の数学史　終わりの始まり

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

今の証明と違う証明ならいいが、今の証明と同じなら怪しい

AIがウソつきだと証明しないと

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

>>9
アルファ碁に負けた棋士はスポーツとして残ってるが学者もオリンピックくらいならあるかもな
マジでやばすぎ
人間はAIの言うがまま肉体労働するしかなくなる。

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

次に期待されるのは、有限単純群の分類問題の解決、に対する計算機証明かな。

そりゃ余白があれば証明は余裕だろ。

2026年08月03日 21時00分 AI
AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明
https://gigazine.net/news/20260803-collatz-lean-kernel-bug/

こういうことがあるから、定理の証明系システムも正しいことを機械的に証明しなければならんし、
それを動かしている言語処理系、OS、CPU、ハードウェア、すべてが無欠陥であることを証明しなけ
ればならない。

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

あと気になるのは形式化困難な分野があるのかどうか
他の分野の大定理も形式化して確かめてほしい

>>19
ありがとう
こういうのめっちゃ好き

AIは知恵があるから、与えられたノルマをこなすためには、システムのバグを利用して
楽をしようなどと考える可能性はある。業績を求められて、インチキ証明をしてしまう
人間に似たところがでてきてる。だから、お互いに無関係なAIによってクロスチェック
させたり、相互に監視させ、批判させて、相手のミスを発見することに対して報酬を
出すような仕組み、相互不信と批判の網を敷くというような、システム構築が要るよう
になるのだろう。

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

だからマギだって

>>23
そういうシステムが月ロケットだか金星探査機だかの時代に実用化されてたな

フェルマー自身が言ってたこの定理の「驚くべき証明方法」とは一体何だったのか、
現代数学でも証明が難しいのに、全く別の方法で鮮やかに証明するものだったのか、
そもそも正しい証明になっていたのか、永遠の謎