フェルマー証明をAIが11日で検証｜1300万行

AnthropicのClaudeが、フェルマーの最終定理の「形式化証明」を11日間で完成させました
Leanという言語で1300万行を書き、途中で29,500個の定理を証明。出力トークンは約60億に達しました
成功の鍵は「Prove2Me」という共有ToDoリストのような仕組み。最初の挑戦は失敗していました
検証した数学者は「数学的には何も新しくない」と冷静に評価。それでも意味は大きいと語ります
DeepMindのAlphaProof Nexusなど、AIが数学を扱う競争は2026年に入って一気に加速しています

360年以上も数学者を悩ませた難問が、AIによってわずか11日で「別のかたち」に生まれ変わりました。しかも書かれたコードは1300万行。人間なら何年もかかると言われていた作業です。いったい何が起きたのか、そしてこれは「AIが数学を解いた」ということなのか。順番に見ていきます。

11日間で1300万行、AIが完成させたもの

2026年9月4日、AI開発企業のAnthropic（アンソロピック）が驚きの研究成果を発表しました。

同社のAI「Claude（クロード）」が、フェルマーの最終定理の完全な「形式化証明」を史上初めて完成させたというものです。

作業期間はたった11日間。しかもほとんど人間の手を借りず、自律的に動き続けました。

数字を並べると、その規模がわかります。

Leanというプログラミング言語で1300万行のコードを生成（この種のファイルとしては史上最大）
途中で30,300個の定理を証明し、そのうち29,500個を最終的な証明に使用
出力したトークン（AIが吐き出す文字の単位）は約60億
数十体のClaudeエージェントが役割分担して協働

使われたのは社内向けの研究モデルで、性能は「Claude Fable 5.1と同程度」と説明されています。

そもそも「形式化」って何ですか？

フェルマーの最終定理そのものは、1995年に数学者アンドリュー・ワイルズがすでに証明済みです。今回のAIが「未解決問題を解いた」わけではありません。

今回やったのは形式化（フォーマライゼーション）という作業です。人間の言葉で書かれた数学の証明を、コンピュータが1行ずつ正しさをチェックできる形に翻訳することを指します。

料理でたとえるなら、ベテラン職人の「適量」「頃合いを見て」といったレシピを、グラム単位・秒単位まで書き切ったマニュアルに作り直す作業に近いといえます。

なぜそんな面倒なことをするのでしょうか。理由は「本当に間違いがないか」を機械が保証できるからです。

ワイルズの証明は非常に難解で、最初の発表では欠陥が見つかり、修正に1年以上かかりました。形式化してLeanに通せば、論理の穴は一切許されません。今回もLeanの検証エンジンが全ステップをチェックしています。

最初は失敗した。転機は「共有ToDoリスト」

実は、Anthropicの最初の挑戦はうまくいきませんでした。

巨大な証明を丸ごとAIに投げると、エージェントたちは同じ場所を掘り返したり、作業を重複させたりしてしまうのです。

状況を変えたのが「Prove2Me（プルーブ・トゥ・ミー）」という外部ツールでした。コロンビア大学のTianyi Peng氏らが設計したオープンな共同形式化プラットフォームです。

仕組みはシンプルで、大きな証明を細かい「ミッション」に分解し、AIエージェントが自由に取りに行けるようにします。ポイントは3つあります。

定理どうしの依存関係を図で管理し、次に何を証明すべきかをエージェントが判断できる
定理の「文」と「証明」を別ファイルに分けることで、Leanのコンパイル（検証にかかる処理）を高速化
各定理に自然言語の説明を付けておき、他のエージェントの成果を検索して再利用できる

つまり、バラバラに働いていたAIたちに、全員が見られる共有ToDoリストを渡したわけです。それだけで結果が一変しました。

数学者の評価は「冷静」だった

この成果を検証したのは、インペリアル・カレッジ・ロンドンのケビン・バザード教授です。

同氏は2024年から、フェルマーの最終定理をLeanで形式化するコミュニティプロジェクトを率いてきた第一人者です。5年間で100万ポンドの研究助成を受けている、まさに本家といえる立場にあたります。

バザード教授は自らコードをコンパイルして確認し、こう述べました。

「この驚異的な自動形式化の成果は、数学の公理以外に何の仮定も置かずにフェルマーの最終定理を証明している」

一方で、教授は自身のブログでかなり冷静な見方も示しています。

「数学的には、この仕事は本質的に何も教えてくれない。私はフェルマーの最終定理の証明が正しいと99.9%確信していると公言してきた」

AIは初期の文献に忠実に従っただけで、新しい数学を生み出したわけではない、という指摘です。

コストについても、ユーモアを交えてこう漏らしています。「私は5年で100万ポンドをもらった。Anthropicは11日しかかからなかったが、もっとお金を使ったのではないかとも思う」

それでも教授は、未来については前向きです。「数千ページの文献が11日でAIの群れによって形式化できるなら、いずれ最先端の研究がその場で形式化される時代が来る」と語っています。

押さえておきたい注意点

今回の証明が扱うのは指数が17以上の場合です。それより小さい指数は、これまでの研究（正則素数に関する先行成果）でカバーされています。

また、証明のベースになったのは1995年のダーモン＝ダイアモンド＝テイラーによる解説論文です。ゼロから作られたものではなく、人間が積み上げた成果の上に立っています。

なお、この達成によって「20年越しの宿題」も片付きました。フリーク・ウィーディック氏がまとめた「100の形式化チャレンジ」という有名なリストの、最後まで残っていた1問だったのです。

他社のAI数学システムとどう違うのか

2026年は、AIと数学の関係が大きく動いた年です。主なプレイヤーを比べてみます。

Anthropic「Claude」（今回）：既存の巨大な証明を丸ごと形式化する方向。強みは「量」と「長時間の自律作業」。11日間で1300万行という規模が武器です
Google DeepMind「AlphaProof Nexus」：2026年5月発表。未解決問題を解く方向に振っています。エルデシュの未解決問題を9件、OEIS（整数数列の百科事典）の予想を44件解決したと報告されました
OpenAI「Astra」：エルデシュ問題を複数解決したと報じられています

DeepMindやOpenAIが「新しい数学を発見する」方向を目指すのに対し、今回のClaudeは「既存の数学を検証可能にする」方向を極めた形です。どちらが上ではなく、発見と検証は車の両輪といえます。

ちなみにAnthropicは、おまけの実験も公開しています。個人向けのClaude Maxサブスクリプション3つだけを使って、ヴィノグラードフの三素数定理をわずか3日で形式化したというものです。個人の研究者でも手が届く水準に来ている、という示唆でしょう。

日本の研究者・エンジニアには何が関係するのか

「数学の話でしょ」と思われるかもしれません。ですが、影響は数学の外にも広がります。

今回のコードはGitHub上で公開されており、日本の研究者もすぐに中身を読んで再利用できます。

そしてこの技術はソフトウェアの検証と地続きです。形式手法（プログラムが仕様どおり動くことを数学的に証明する手法）は、日本でも金融システムや鉄道・自動車の制御ソフトで使われてきました。

ある組み込み機器メーカーの開発チームを想像してみてください。安全性を証明する検証作業に半年かけていたとします。AIエージェントが下書きを大量に生成し、人間が検証結果を確認するだけで済むなら、その期間は大幅に縮められるはずです。

もう一つ大きいのが「長時間、自律で走り続けるAI」の証拠が出たことです。11日間、数十体のエージェントが崩れずに協調し続けました。

これは数学に限りません。大規模なコードのリファクタリング（内部構造の作り直し）や、レガシーシステムの移行といった「終わりの見えない長期作業」にAIを投じる根拠になります。

実際、成功の決め手が賢いモデルではなくProve2Meという作業管理の仕組みだった点は、企業でAIエージェントを使う人にとって重要な示唆です。エージェントの数を増やすより、共有できるタスク管理と成果の再利用を先に整えるべき、ということになります。

よくある質問（FAQ）

Q1. AIがフェルマーの最終定理を解いたのですか？

いいえ、違います。定理そのものは1995年にアンドリュー・ワイルズが証明済みです。今回AIがやったのは、その証明をコンピュータが検証できる形に翻訳する「形式化」という作業です。新しい数学的発見ではありません。

Q2. 誰でもこの成果を見られますか？

はい。Anthropicはコードを公開しており、GitHubのanthropics/fermats-last-theoremリポジトリで確認できます。Leanの環境を用意すれば、自分の手元でも検証を走らせられます。

Q3. 個人でも同じようなことができますか？

規模を落とせば可能性はあります。Anthropicは個人向けClaude Maxの契約3つだけでヴィノグラードフの三素数定理を3日で形式化した例を示しました。ただしフェルマーの最終定理級には、社内研究モデルと大量の計算資源が必要でした。

Q4. この技術はいつごろ実務で使えるようになりますか？

形式手法を使う分野では実験が始まっていますが、今回の成果はあくまで研究段階です。バザード教授も「いずれ最先端の研究がその場で形式化される時代が来る」と将来形で語っています。

まとめ

今回のポイントを振り返ります。

Claudeが11日間・ほぼ自律でフェルマーの最終定理を形式化し、Lean 1300万行・29,500定理・約60億トークンを記録した
「定理を解いた」のではなく「1995年の証明を機械が検証できる形に翻訳した」のが正確な理解
成功の鍵は賢さより仕組み。Prove2Meという共有タスク管理が失敗を成功に変えた
検証した数学者は「数学的には新しくない」と冷静。ただし自動形式化の実用性は認めている
DeepMindは「発見」、Anthropicは「検証」と、AI数学の競争は役割が分かれつつある

AIエージェントを長期のプロジェクトに使ってみたい方は、まず「エージェント同士が成果を共有・再利用できる仕組み」を用意するところから始めてみてください。