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

>>81
すごい幸せな社会だよなそれ
おめえ向いてねぇんだよって向いてないやつが無駄な努力をしなくて良くなる

４光年先にいる宇宙人の超文明は我々の科学の水準を遙かに超えた想像を絶する先進の世界だったとする。
たまたまそこと通信ができる時代になると、超文明からいろんな知識を問い合わせて得ることで、
人類はうんと文明を進めることができるようになり、たとえばそれまでAIでも解決できなかった
困難な問題への解を教えて貰って論文が書けてフィールズ賞が貰えたりするようになるのだ。

資本主義社会は放置すると

底辺への競争を行う
フィジカルAIが安くて優秀になると　企業はフィジカルAIを雇い　人を雇わなくなる

放置すると起きるのが大失業社会

かつては無理だった共産主義も現実味を帯びてきて
フィジカルAIに全部任せればイイジャンっていう話だが

フィジカルAIに命令する権利をどうやって持つのかって話で
作る能力もない場合・・・その権利がそもそもない

つまり大失業社会の負の側面だけが襲い掛かるリスクがある

ないんだよｗｗｗ
共産主義者のトップ本音はただたんに追放されない絶対的な群れのボスに永遠にとどまりたいだけなんだからｗｗｗｗ
間違えても歯車になりたいわけではないｗｗｗｗ

>>15
中華ロボットも優秀なので、その内肉体労働もなくなる。そうすると無駄な人間の排除が始める。

共産党のあほに使えるロボット奴隷を作ったらまあ間違いなくそうなるなｗｗ自信あるｗ

でもｗｗｗｗ共産主義ｗ共産党に都合がいい嘘はったりを垂れ流す御用学者としての職は一時的に大幅増だろうなｗ
ぶっちゃけ占いがそういうものなんだからよｗ

ネット工作員もそういうお仕事の一種だよなｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗ

>>51
>無限降下法の適用限界を見誤ったと思われる
そういう意見よく見るんだけど、n=4のときの反例は(x^2)^2+(y^2)^2=(z^2)^2だからx^2,y^2,z^2がピタゴラス数になるという性質をふんだんに利用していて、無限降下法の適用限界も何も、そもそも他のnの証明でn=4のときのような無限降下法に持ち込めそうな気がしない。
何をどう見誤ったというんだろう

それはさておき、フェルマーはn=4の証明のあとにn=3の証明に取り掛かっていた形跡があるようで、本当に一般のn>2で証明していたなら個別にn=3の証明に手を出す理由がない。本人もn=4以外の証明はできていないことに気付いていたんだろうね

> 1300万行のLeanコード

確かに余白が足りなさそう

私は素晴らしい証明を生成できたが、それを書き出すには今のSSDは高すぎて容量が足らない。

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

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

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

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

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

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

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

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

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