2026年9月4日、Anthropicは学術界を揺るがす発表を行った。数十のエージェントからなるAI群が、わずか11日間で「フェルマーの最終定理」の完全な機械検証を完了したというものだ。これに対し、インペリアル・カレッジ・ロンドンの数学者チームは100万ポンドの研究資金を獲得し、同一の形式化タスクに丸5年の期間を予定していた。
350年以上にわたり人類を悩ませてきたこの数学の難問は、1995年に英国の数学者アンドリュー・ワイルズ（Andrew Wiles）によってすでに証明されている。今回繰り広げられた「11日対5年」の戦いは、数学そのもののフロンティアを押し広げたわけではない。
真に打ち破られたのは、知識の正しさを担保するために人間の専門家に依存し続けてきた、従来の信頼モデルである。長大な論文の評価は、「人間による数年がかりの査読（見落としの余地あり）」から、「機械が論理の破綻を数分で検証する世界」へと決定的な転換点を迎えた。
350年の難問が浮き彫りにした「人間の査読」の限界
フェルマーの最終定理の歴史を振り返ると、それは人間の査読システムが破綻を繰り返してきた記録でもある。1908年にドイツで設立されたヴォルフスケール賞は、証明に対して10万金マルクの懸賞金を拠出した。これを受け、初年度だけで621件もの解答が寄せられたが、そのすべてに致命的な誤りが見つかった。
人間の脳は、膨大で複雑な論理を処理する際、本質的に見落としを免れない。1993年6月、ワイルズはケンブリッジのニュートン研究所で3夜連続の講演を行い、フェルマーの最終定理を証明したと世界に向けて発表した。しかしそのわずか2か月後、査読者が定常的な確認の過程で突きつけた鋭い質問によって、論理の骨格に致命的な欠陥が存在することが露呈した。
ワイルズはその後、証明の修復に丸1年の苦闘を強いられ、一時は断念すら考えた末に、1995年5月にようやく129ページに及ぶ決定版の論文を発表した。少数のトップクラスの数学者が密室に集まり、100ページを超える難解な手稿を精読する——そうした手作業による検証は、当時すでに人間の認知的限界に達していた。
図：Anthropic公式発表ページのヘッダー画像。出典：Anthropic
11日間で書き上げた1300万行の機械コード
難解な数学記号の連なりを、いかにして機械に検証させるのか。鍵となるのが「形式化（formalization）」である。人間の直観や論理の飛躍を含む散文調の証明を、句読点一つに至るまで誤りが許されない機械コードへと翻訳する作業だ。かつてこの作業は、情熱的な一部の専門家のみが取り組む過酷な重労働だった。
インペリアル・カレッジ・ロンドンのKevin Buzzard教授は、フェルマーの最終定理の形式化を5年計画で進めるコミュニティプロジェクトを率いていた。翻訳の手順を示す「ブループリント（設計書）」を作成するだけで、86ページもの文書が書かれたほどだ。
Anthropicの社内研究モデルClaudeは、Prove2Meプラットフォーム上でこの長大なスケジュールを2週間足らずに圧縮した。1995年の古典的で整理された証明ルートを踏襲しつつ、1,300万行を超えるコードを生成。この分量は、同プラットフォームの公式数学ライブラリ全体の5倍以上にも達する。
コードには30,300件の定理・補題の証明が含まれ、最終的に29,500件が証明グラフに組み込まれた。数十のAIエージェントが休むことのない歯車のように並行して連携し、人間の曖昧な直観を細かく砕いて、機械が1行ずつ実行可能な論理の連鎖へと落とし込んだ。
30万ドルの計算コストで買い取った「絶対的確実性」
産業規模の計算資源が投入されたことで、多額の人件費は計算資源のコストへと置き換わった。Buzzard教授チームの5年計画は100万ポンドを要し、研究者の知的労力、給与、そして長期間のコミュニケーションコストに依存していた。
一方、Claudeによる今回の検証では、約60億の出力トークンが消費された。現在の公開API価格に基づくと、その費用はおよそ30万ドルに相当する。人間なら5年を要する絶対的な確実性を30万ドルの計算資源で買い取ったことで、最先端研究のコスト構造は不可逆的な変革を迎えた。
もちろん、機械が最初から無謬だったわけではない。初期の試行ではエージェント同士の連携が崩れ、プロジェクトの状態を見失う場面もあった。だがシステムは試行錯誤を通じて速やかに調整を行い、失敗した試行も最終コードの非定型部分の約7%に貢献した。Anthropicの研究者は最上位の指示を与えるだけで、具体的なデバッグや問題解決の大部分は機械自身が自律的に処理した。
図：Prove2Meプラットフォーム上の証明ルートDAG。Claudeが補題を分解し段階的にFLTへ迫る様子を示す。出典：Anthropic
科学の信頼基盤はコンパイラへと委ねられた
Kevin Buzzard教授自身が1,000万行を超えるコードを検証し、コンパイラはエラーなく通過した。差分比較ツールによっても、すべての定理の記述が既存の数学ライブラリと完全に一致することが確認された。これにより、20年の歴史を持つ「100の形式化課題」ベンチマークリストはすべて完了したことになる。
Buzzard教授が述べたように、数学的な新定理が発見されたわけではない。しかし自動形式化の分野において、今回の成果は極めて強力な実証結果をもたらした。129ページに及ぶ難解な証明がソフトウェアのソースコードのようにコンパイル可能になったとき、学術界の信頼ネットワークは根底から更新される。
かつて、ある定理が正しいと信じられたのは、権威ある碩学たちの推薦があったからだ。いまや、そうした中央集権的な権威モデルは解体されつつある。コードがコンパイラを正しく通る限り、真理の証明に人間の後ろ盾は必要ない。コンパイラが最後の砦としての役割を引き受けている。
参考リンク：
- Anthropic Research
- HN 議論
