Claudeが「フェルマーの最終定理」の完全なコンピュータ検証済み証明を11日で自動生成

>この証明をこれほどの速さで生成できたことは、数学の広い範囲を形式化することが今や可能であることを示しています。これにより、一般的な数学の証明の集合における誤りを発見できる可能性があり、また新しい研究の査読の負担を軽減することもできるでしょう。

^ この部分は、私の意見では最初の数段落にあるべきでした。これがなぜ重要なのかを説明することは、そんなに後ろの方にあるべきではありません。

「この証明は、私自身がKhare、Taylorなどのアイデアに従って形式化してきた現代的な証明ではなく、1995年のDarmon–Diamond–TaylorによるWiles–Taylor–Wilesの議論の解説であり、Langlands–Tunnellの定理とRibetのレベル低下定理を経由するものです。Anthropicのリポジトリは、Fontaine理論（ガロア表現の平坦な変形を研究するため）を発展させ、Eisensteinイデアルに関するMazurの研究を、p>=17の位数の点を持つFrey曲線は存在しないと結論するのに十分な範囲で発展させています。これは、彼らのFLTの証明がp>=17に対してのみ機能することを意味しますが、FLTは既にBest-Birkbeck-Brasca-Rodriguezによって奇数正則素数に対して形式化されており、最小の非正則素数は37なので、すべて問題ありません。」

これを読んでいる数学者に質問です: 上記はあなたにとって何か意味を成しますか?

そう尋ねるのは、私はコンピュータ工学、プログラミング、ハードウェア仕様などに関するほとんどの技術資料を読むことができるからです。詳細を完全に理解していなくても、かなりよく追うことができます。だから、プロの数学者が上記を見て、経験豊富なソフトウェアエンジニアがコンピュータ関連のことを理解するように、まだ意味を理解できるのかどうか疑問に思います。

>その過程で、1300万行のLeanコードを書き、29,500の中間定理を証明しました。

かなり驚異的です。正しさを示すことができるものは何でもモデルによって実行できるという考えをさらに裏付けるものだと思います。

>エージェントのチームは2週間弱で証明を完了し、Claude Fable 5.1にほぼ相当する汎用内部研究モデルから約60億の出力トークンを消費しました。

APIレートで$50/M出力トークンだと、これは約30万ドル（入力/プリフィル・トークン用に少し追加）のコストになるでしょう。

余談ですが、サイモン・シンのこの本を強くお勧めします。

https://en.wikipedia.org/wiki/Fermat's_Last_Theorem_(book)

1300万行のコードですが、Leanの証明システムの潜在的な問題を利用しなかったと確信できますか?

AIツールがスケールするにつれて、この種の発表をますます目にするようになるでしょう。エージェント型コーディングが印象的である一方で、医療、数学、物理学の研究の価値提案には及びません。

私は楽観的に、AIの努力のおかげで、生涯のうちに世界的な「万能薬」の出現を目撃することを期待しています。費用対効果の高い大規模遺伝子工学、あらゆる病気の治療法、おそらくは老化の治療法さえも。

未来は美しくもあり、恐ろしくもあります。

よし、それではP = NP?を解かせるために、狂暴なエージェントの群れを動員しよう!

自動証明検証がこれほど高性能で安価になるにつれて、数学コミュニティのほぼ全員が真実だと仮定している証明のうち、いくつが偽であると証明されるのだろうかと思います。そして、それは些細で修正しやすい誤りではなく、推論における根本的な欠陥によるものでしょう。