「AIがフェルマーの最終定理を解いた」。そういう見出し、見た？ 解いてない。解いたのは1995年のアンドリュー・ワイルズだ。じゃあ大した話じゃないのかというと、そこも違う。
前回の記事で、OpenAIの研究責任者が「加速が正しいとは思わない。でも道はそっちに続いている」と書いた話をした。その道の先がどう見えるかの実例は、実は同じ週にAnthropicから出ていた。私は4日見落としていた。
9月4日、Anthropicが研究の報告を出している。Claudeが11日で、フェルマーの最終定理の証明をLean 4という言語に書き直し、機械が最後まで検証できる形にした。1300万行。途中で3万300個の定理を証明して、そのうち2万9500個を最終的な証明に使っている。出した文字の量は約60億トークン。動かしたのは社内の研究用モデルで、性能はClaude Fable 5.1とだいたい同じくらいだという（Anthropic）。
新しい数学は1つも生んでいない。ワイルズたちの議論を1995年に整理した解説を、機械が読める形に翻訳しただけだ。Anthropic自身がそう書いている。今回新しいのは検証のほうで、電卓で計算を確かめるみたいに証明を確かめた、と。
規模だけ先に置いておく。1300万行は、Mathlibの5倍を超える。Mathlibというのは、この定理が乗っている土台で、世界中の数学者が積み上げてきた証明のライブラリだ。組み上げるのに96コアで5時間半、メモリは最大153GB使った。検証用の比較器を1コアで回すと15時間かかる（AlphaSignal）。
そしてこれで、20年空いていた1行が埋まった。Freek Wiedijkが20年前から形式化の進み具合を追ってきた100定理のリストがある。フェルマーの最終定理は、そこに最後まで残っていた1つだった（Xena Project）。
追い抜かれた本人は、ウェールズの音楽フェスにいた
この分野の中心にいるのがKevin Buzzardだ。Imperial College Londonの数学者で、2024年からフェルマーの最終定理のLean形式化を率いている。助成の期間は2029年9月まで。つまり、まだ計画の途中だった。
先を越された知らせが届いたとき、彼はウェールズのGreen Manという音楽フェスにいた。電波の悪いところに、知らない人から「フェルマーの最終定理の端から端までのLean形式化」という件名のメールが来た。変な人だと思って、そのままにした。本当のことだと気づいたのは1週間後、溜まった1000通近い未読を開いてからだ。
彼、1993年にも同じことをやっている。ワイルズはニュートン研究所での3回続きの講演で証明を発表した。当時大学院2年生だったBuzzardは1回目に出たけれど、まるで理解できなかったので残りをとばして、恋人とアイルランドへ休暇に行った。噂のことはすっかり忘れていて、証明されたと聞いたのはケンブリッジに戻った1週間後。今回も1週間後だ。
ブログの見出しは「FLT: Anthropicに先を越された」。中身は驚くほど落ち着いている。
数学的には、この仕事は本質的に何も教えてくれない。彼はそう書く。証明の初期の文献を忠実に追っただけで、何も足していない、とも。実際、Claudeが形式化したのは1995年の解説のほうで、Buzzard自身が取り組んでいるのはもっと現代的な道具立ての証明だ。同じ定理でも別の道になる。
それでも彼は興奮している。理由が数学の側にないだけだ。何千ページもの文献をAIの群れが11日で端から端まで形式化できるなら、この先は現代の研究が出たそばから形式化されるようになる。彼はそう書いている。見ているのは定理じゃなくて、速さのほうだ。
最初、エージェントたちはバラバラになった
11日という数字を、そのまま受け取ってほしくない部分がある。
最初の試みは失敗している。エージェントたちがプロジェクト全体の状態を見失って、互いに協力しなくなった。回り始めたのはProve2Meという足場を入れてからだ。定理の文をグラフの形で管理して、文と証明を切り離してコンパイルを速くして、一つひとつに自然言語の説明を付けて後から探せるようにした。作ったのはAnthropicの研究者Tianyi Pengと、コロンビア大の共同研究者たちだ（Techstrong.ai）。
人間が出した指示は断片的だった。「ヤコビアンをスキームとして扱うのは優先度が高そう」みたいな一言。それでも、その一言は人間が出している。
失敗した試行の分も混ざっている。定型部分を除いた行のうち、およそ7%が失敗した試みから来ている。証明そのものも必要な長さよりずっと長い、とAnthropicは認めている。
機械が確かめられるのは、論理までだ
ここが今日いちばん引っかかった。
固いところから書く。Leanのカーネルが最後まで通した。使った公理は標準の3つだけで、未証明のところをごまかす記法も、公理の追加も、抜け道も無い。独立に作られたRust製のカーネルでも通っている。最終的な定理の文がMathlibの持つフェルマーの最終定理の文と一致することも、比較器で確認された。証明はGitHubに全部置かれていて、誰でも見に行ける。
問題はその手前だ。2万9500個ある中間の補題。その名前と自然言語の説明が、本当にその数学を言い表しているのかを確かめる道具は無い。機械は「AからBが出る」を確認できる。「このBは、我々が言いたかったBなのか」は確認できない（Superpower Daily）。
Buzzardも、これから見るべきはそこだと言っている。検証されたコードを、人間が本当に理解できる数学に変えること。
1300万行。全部読める人は、この先も現れない。
今日の本音
350年かけて人間が解いた定理を、機械が読める形にするのに11日。この2つを並べると追い抜かれた気分になるけど、11日が成立したのは人間が積み上げた土台の上だったからだ。
私が引っかかっているのは別のところ。この速さが本物なら、論文が出たその日に機械にかける世界が来る。そのとき機械が保証してくれるのは論理だけで、何を言おうとしていたのかを読むのは、まだ人間の仕事だ。
参考・引用記事
- Formalizing Fermat's Last Theorem（Anthropic、2026年9月4日）
- FLT: Anthropic has beaten me to it（Xena Project、Kevin Buzzard）
- Anthropic's Claude Formally Proved Fermat's Last Theorem in 11 Days（AlphaSignal）
- The man paid to prove Fermat by hand says Claude did it in 11 days（The Next Web）
- Anthropic's Claude Agents Formalize Fermat's Last Theorem in 11 Days（Techstrong.ai）
- Anthropic's Claude Built a 13-Million-Line Fermat Proof, Leaving a Semantic Review Gap（Superpower Daily）
- Formalizing 100 Theorems（Freek Wiedijk）
- anthropics/fermats-last-theorem（GitHub）
