Claudeがフェルマーの最終定理をLeanで形式化、1300万行を11日で完成

AI開発企業のAnthropicは2026年9月4日、AI「Claude」がフェルマーの最終定理についてコンピューターで最初から最後まで検証できる証明を完成させたと発表した。フェルマーの最終定理は、nが2より大きい整数のとき、正の整数a、b、cがaのn乗+bのn乗=cのn乗を満たすことはない、というものだ。数学者アンドリュー・ワイルズが1995年に129ページの証明を発表してから30年余りが経つが、その論理を一からコンピューターに検証させた例はこれまでなかった。Claudeは11日間にわたってほぼ自律的に作業し、証明支援システム「Lean」で約1300万行のコードを書き上げた。

Anthropicの研究者でAIによる数学の形式化を研究するティエンイー・ペン氏がこの取り組みを主導した。Claudeは作業の過程で約3万300件の定理をコンピューターで検証可能な形に証明し、最終的な証明では約2万9500件を実際に使用した。生成されたコード量はLean向け数学ライブラリ「Mathlib」の5倍以上に達する。数十のClaudeエージェントが並行して概念の定義や中間定理の証明を分担し、成果を積み上げながらより難しい命題の証明へと進んでいった。当初は各エージェントが巨大なプロジェクトの進捗を把握できず成果を共有できないという失敗も重なり、最終的な証明の非定型部分の約7%は、こうした失敗した試みに由来するという。

「形式化」とは何か

人間向けの数学の証明論文は、読者にとって「明らか」と判断できる手順を省略することが多い。しかし証明支援システムのLeanにその正しさを確認させる場合、省略は許されず、あらゆる論理の飛躍を厳密に書き下す必要がある。既存の証明をこの形へ書き直す作業が「形式化」だ。1カ所でも論理のつながりが崩れれば、その先の結論全体が成立しなくなる恐れがあるため、形式化された証明はLeanによる機械的なチェックを通過して初めて、人間の目視確認に頼らない客観的な正しさの保証を得られる。今回の証明はLeanが持つ標準的な3つの公理だけに依存し、証明を一時的に省略する「sorry」のような未完成箇所も一切含まれていない。数学ライブラリMathlibに収録された定理の記述と、Claudeが証明した対象が一致することも比較ツールで確認済みで、Rust製の独立したLeanカーネル「nanoda」による検査でも100万件超の宣言がエラーなく通過したという。

なぜフェルマーの最終定理が象徴的な題材なのか

フェルマーの最終定理は、17世紀のフランスの数学者ピエール・ド・フェルマーが著書の余白に書き残した命題だ。フェルマーは「この命題には真に驚くべき証明を発見したが、この余白はそれを書くには狭すぎる」という有名な言葉を添えたが、その証明は後世に残されなかった。以来350年以上にわたり数学者たちが証明に挑み、1908年には現在の価値で100万〜200万ドル相当とされる懸賞金がかけられ、最初の1年だけで621件もの誤った証明が寄せられた。1993年6月、アンドリュー・ワイルズは3日間の連続講演で証明を発表したが、査読の過程で致命的な欠陥が指摘され、弟子のリチャード・テイラーとともに1年がかりで修正し、1995年5月にようやく完全な証明を発表した。この証明は129ページに及び、正しさの確認だけで数カ月を要した。なお、ワイルズの証明の核となる「谷山・志村予想」(モジュラー性定理)は、日本の数学者である谷山豊氏と志村五郎氏が1950年代に提起したもので、フェルマーの最終定理は日本の数学とも深い縁を持つ。今回Claudeが形式化したのも、この谷山・志村予想を基盤とするダーモン・ダイアモンド・テイラーによる簡略版の証明筋道だ。

この驚くべき自動形式化の成果は、Anthropicの研究者によればわずか11日間で達成されたもので、数学の公理以外に何の仮定も置かずにフェルマーの最終定理を証明している。この過程で代数、調和解析、幾何学、数論の自動形式化を目にすることになり、AIによる自動形式化の成果物がすでに積み上げられるほど頑健になっていることも分かる。

• 作業期間: 11日間(ほぼ自律的な作業)
• 生成したLeanコード: 約1300万行(数学ライブラリMathlibの5倍以上)
• 証明した定理: 約3万300件(うち最終証明で使用したのは約2万9500件)
• 消費した出力トークン: 約60億(Claude Fable 5.1に近い汎用研究モデルを使用)
• 依存する公理: Leanの標準的な3公理のみ、未証明箇所「sorry」はゼロ

Claudeが実際にやったこと、そしてその限界

ここで押さえておくべきなのは、Claudeがワイルズの証明を独力で「発見」したわけではないという点だ。数学的な推論そのものは1995年にワイルズらが確立したものであり、Claudeが行ったのはその筋道(の簡略版)を、Leanが理解できる厳密な記号の連なりへと書き直し、コンピューターに検証させる「形式化」作業である。これは最近話題になったリーマン予想をめぐるAIの研究——新しい数学的知見を生み出そうとする試み——とは性質が異なる。Anthropicは今回の成果について、新規性があるのは新しい数学を生み出したことではなく、既存の証明の「検証」の部分だと明確に位置づけている。作業には数学的な協働基盤「Prove2Me」が使われ、定理同士の依存関係を有向非巡回グラフ(DAG)で管理することで、複数のClaudeエージェントが次に取り組むべき定理を把握できるようにした。定理の内容と証明を別ファイルに分けてコンパイルを高速化し、各定理に自然言語の説明を付けて再利用しやすくする工夫も効いたという。人間による介入は、ペン氏による「スキーム上のヤコビアンを優先すべきだ」といった高レベルの指示にとどまっている。それでも初期の試行では、エージェントがプロジェクト全体の状態を見失い、互いの成果をうまく再利用できなくなる失敗が繰り返された。AIの能力そのものに加えて、どこまで終わり次に何を証明すべきかを管理する仕組みが、長期にわたる複雑な作業には不可欠だということが今回の教訓だ。

AIが数学の証明を量産できるようになるほど、その正しさを人間だけで確認する負担は増していく。Anthropicは、人間向けの論文と並行してコンピューターで検証可能な形式化済み証明を用意することが、今後は一般的になっていくと見込んでいる。この分野を長年率いてきたインペリアル・カレッジ・ロンドンのケビン・バザード氏も、今回の成果を現代の数学文献を自動形式化する技術への大きな一歩だと評価し、既存の数学の誤りをあぶり出し、査読者の負担を軽くし、AIが生成した数学を厳密に検証する手段にもなると述べている。バザード氏は2024年からフェルマーの最終定理をLeanで形式化する共同プロジェクトを率いており、初期段階の作業計画だけで86ページに達し、形式化には数年かかると見込まれていた。

日本の読者にとってこの一件は、単なる海外の技術ニュースにとどまらない。フェルマーの最終定理を解く鍵となった谷山・志村予想が日本発の着想である以上、その最終的な機械検証にAIが挑んだという事実は、日本の数学コミュニティにとっても無縁ではない。国内の大学や理化学研究所などの研究機関にとっては、Leanのような証明支援システムとAIエージェントを組み合わせた形式手法を、純粋数学だけでなく金融工学や自動運転、産業制御システムなど正しさの保証が欠かせない分野のソフトウェア検証に応用する好機となる。国内のAI企業やソフトウェア企業も、既存の設計文書やコードベースを形式的に検証可能な仕様へ書き直す作業にAIエージェントを充てられないか検討する価値がある。ただしAnthropic自身が強調する通り、これは新しい数学を「発見」する能力ではなく、既存の正しさを「保証」する能力であることを見誤ってはならない。