【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の証明結果を検証するのが
ますます大変になる。

その検証もＡＩで機械化
せねば。　そのレポートは
検証対象以上に膨大なレポートに
なるかも。

人間は、ＡＩに解けない問題を
与えて、結果だけを応用して
実用化する方向に行くかも。

真理かどうかは実用化できて
効果を産むかどうかになる。

LEANは帰納的定義でいろんな概念組み上げて証明作るんだから
ある意味無限降下法よ

>>74
現場猫理屈？やん
役立つから真理でヨシ！ｗ