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

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

ヒルベルトが聞いたらびっくりするだろな。まさか形式論理が現実に実用化されるなんて思ってなかったというだろうと思う。

ヒルベルトは形式主義派だったので何の驚きもないはず
ペアノの公理を拡張していけばいいと思っていたわけだし
証明は有限な手順に抑え込めると考えていた
むしろ完全勝利という感じだろう
計算機数学の方の論理主義の隆盛の方が驚きだろう
あと直観主義で証明できる数学範囲が意外に多いことにも驚いてるはず

数学がいう有限でできるということと、それが現実に実行できるということの間には大きな隔たりがある。
ゲームの理論から、囲碁が先手必勝であるか後手必勝であるか必ず引き分けに持ち込めるかの3通りだとして、
それのどれであるかを決定するのは大変で、厳密な証明はまず無理だろう。囲碁までいかずとも、8ｘ8盤の
オセロが先手必勝か後手必勝か必ず引き分けにできるかのどれかを決定することは人力では無理。
＃もしもある命題の証明が存在してそれを有限長の記号の列で記述が可能であるとすれば、
「有限の手数」で必ずその記号の列を具体的に割り出すことが機械的にできるが、
それは現実的には到底無理な話だ。
また、もしも「ある命題の証明が存在しない」ことの証明が存在していて
それを有限長の記号の列で記述できるのだとすれば、
その記述もまた有限の手数で見いだせることになるが、
もちろんこれも現実的には到底実行することは無理だ。
有限だといっても場合の数が多すぎるので。

有限の立場をまるで理解できてない

>>83
先進文明は次世代AIみたいな物を開発してそれのおかげで地球人には未知の法則の発見も含めかなり先に行ってるはず
我々がコンピュータを駆使して昔の人が手計算では到底出来なかったことを日々しているのと同じ

形式化ってどういうこと？

>>96
オセロは引き分けという結論が出たでしょ

オセロは引き分け、を示すことは人力では無理だろ。