Claude AIがフェルマーの定理を11日間で証明、史上最大のLean証明を生成

AIが358年越しの数学的難問を11日間で形式証明——歴史的マイルストーン

2026年9月4日、AI開発企業Anthropicは、自社の大規模言語モデルClaude AIが、数学史上最も著名な難問のひとつであるフェルマーの最終定理（Fermat's Last Theorem, FLT）の、史上初となるコンピュータ検証済みの完全な形式証明を生成したと発表した。その所要期間はわずか11日間。AIが高度な数学的推論を自律的に遂行できることを世界に示した、歴史的な瞬間である。

フェルマーの最終定理とは、「n が 2 より大きい整数のとき、xⁿ + yⁿ = zⁿ を満たす正の整数の組 (x, y, z) は存在しない」という命題だ。1637年頃にピエール・ド・フェルマーが「この命題の証明を発見したが、余白が狭すぎて書ききれない」と記したことで有名となり、以来358年にわたって数学者たちを魅了し続けた。1995年にアンドリュー・ワイルズがついに証明を発表したが、その証明は129ページに及び、内容の検証には数ヶ月を要した。

今回Claudeが成し遂げたのは、ワイルズの証明を新たに発見したのではなく、その証明をLean 4というプログラミング言語で完全に形式化し、コンピュータが一行一行自動検証できる形に変換したことだ。これは「オートフォーマライゼーション（自動形式化）」と呼ばれる分野における空前のブレークスルーとなった。

プロジェクトの全貌：数字が語る偉業の規模

驚異的なスケール

11日間、ほぼ自律的に動作したClaudeは、FLTの最初のエンドツーエンドのコンピュータ検証済み証明を生成した。その過程で1300万行のLeanコードを記述し、2万9500の中間定理を証明した。

Anthropicのリサーチポストによれば、このランは1300万行のLeanコードを生成し、合計3万300の定理を証明（そのうち2万9500が最終証明に使用）し、約60億の出力トークンを消費した。

13百万行のLeanコードによるClaudeの証明は、この定理が依拠する数学的証明のコミュニティ主要ライブラリ「Mathlib」の5倍以上の規模を誇る。Anthropic自身も、この証明を「史上最大のLean証明」と位置づけている。

マルチエージェント協調による自律動作

数十のClaudeエージェントが協調して概念を定義し、中間定理を証明し、それらの定理を活用してさらに困難な命題を証明していった。

人間からの数学的なインプットは、Tianyi Pengからの高レベルな指示（「スキームとしてのJacobianが優先度高そう」「Mazurの定理を早めに進めて」といった程度）に限定されていた。

プロジェクトはProve2Meプラットフォーム上で8月7日早朝に開始された。そして11日後の8月18日午前2時00分57秒（UTC）、FLTのルートカードがprove2me上で「PROVED」と表示された。

Prove2Meプラットフォームの役割

プロジェクトが成功したのは、コロンビア大学のTianyi Pengとその共同研究者が設計したオープンな数学形式化プラットフォーム「Prove2Me」を導入したことによる。Prove2Meはエージェントが次に取り組むべき証明を判断するための有向非巡回グラフ（DAG）を維持しており、メモリ劣化の緩和と複数エージェントの並列作業を可能にした。

Claudeの初期の試みはいくつか失敗した。エージェントたちは初期段階では一定の成功を収めたものの、プロジェクトの状態を把握できなくなり、効果的な協調が停止した。これらの失敗した試みも最終的な証明の非定型コードの約7%を占めている。

専門家の見解：数学界の反応

AnthropicはImperial College LondonのKevin Buzzard数学教授と証明を共有した。Buzzardは次のように述べている。「この驚くべき自動形式化の成果は、Anthropicの研究者によれば11日間しかかからなかったとのことで、数学の公理以外の仮定なしにフェルマーの最終定理を証明している。」

Buzzardはさらに踏み込んで、「FLTの自動形式化が今や可能であるなら、我々は現代の数学文献の自動形式化に向けて大きな一歩を踏み出した」と述べた。

Buzzardはまた、「代数、調和解析、幾何学、数論にわたる自動形式化が実現され、AIによる自動形式化の成果物が他の研究に活用できるほど堅牢になったことを示している。この証明は多層的だ」とも語っている。

Lean形式化に長年取り組んできたBuzzardは、この成果が専門家の予測をはるかに上回る速さで達成されたと語った。

技術的背景：形式証明とは何か

Anthropicの研究プロジェクトはワイルズの証明を「形式化」したものだ。つまり、コンピュータが自動的に検証できる形式に変換したということだ。証明の形式化は人為的なミスの可能性を排除し、数学者間の情報共有を容易にするという利点がある。

形式化された証明は、Leanと呼ばれるプログラミング言語で記述されたコードスニペットの形をとる。これは数学者が仮説を検証するために使用する専門的な構文だ。

形式証明の最終的な状態として、ルートカード「fermat_last_theorem」——xⁿ + yⁿ = zⁿ の正の整数解は n > 2 では存在しないという基本命題——がProve2Me上で「Proved」と表示されている。これはその依存関係ツリー（Mazur、Ribet level-lowering、Langlands–Tunnell、最小R=T定理、3–5スイッチなど、すべてMathlib上に構築）の約3万のカードすべてが、機械検証済みのLean証明を持つことを意味する。

ビジネス視点：企業・経営者にとっての意味

このマイルストーンは自動形式化における重要な進歩を示しており、複雑な数学的予想の検証をこれまでの数ヶ月かかる手動プロセスから、迅速なAI駆動の自動ワークフローへと移行させるものだ。

スマートコントラクトの監査や安全性が重要なソフトウェアも、同様の手法を採用するケースが増えている。テストスイートは思いついたケースに対してコードが動作することを証明するが、形式証明は仕様が許すすべてのケースで動作することを証明する。

このことは、「AIを活用したサイエンス」系スタートアップが独自モデルの優位性を訴える際の問いかけを変える。今やどんなAIサイエンス系創業者も、「適切なオープンソースの足場さえあれば、ClaudeやGPT-6を使っても同じことができてしまうのではないか？」という問いに答えなければならない。

Prove2Meが無料のオープンツールとして存在していたことが、Anthropicの独占的なブレークスルーではなく、このプロジェクトを可能にした鍵であり、数学・科学に特化したAIスタートアップの「堀（モート）」は厚くなるどころか薄くなったと見ることもできる。

消費者・生活者視点：一般の人々への影響

Claudeはフェルマーの最終定理の現代的証明をLeanに変換し、証明アシスタントが人間の数学的レビューだけに頼らず、すべての論理的依存関係を検証できるようにした。この技術は将来的に、医薬品の安全性検証、航空・自動車の制御システムの確認、金融商品のロジック検証など、人々の生活に直接関わる重要システムの信頼性向上に貢献する可能性がある。

形式的検証は定理が公理から導かれることを確立するが、定理が科学的に興味深いこと、選択された定義が意図した実世界の概念を捉えていること、あるいは1300万行の証明が人間にとって理解できることを保証するものではない。Anthropic自身も、形式証明は人間が読める数学的説明を補完するものであって、置き換えるものではないと論じている。

国際比較：AI数学研究の潮流

このマイルストーンは、AnthropicがLLM（大規模言語モデル）駆動の別の数学的進歩を詳述した約1ヶ月後に達成された。同社はリーマンゼータ関数に関する新たな知見をClaudeが発見したと報告しており、この関数はリーマン予想という世界最難関の数学的問題の核心に位置している。

競合のOpenAIも、最新のモデルを数学研究の発展に活用している。同社は最新モデルを使っていくつかのErdős問題を解き、理論計算機科学の未解決問題をいくつか絞り込んだと伝えられている。

こうした動きは、AI各社が汎用的な言語能力の競争から、科学的発見・数学的推論への深化という新たな競争軸に移行しつつあることを示しており、学術界とAI産業の融合が加速していると見られる。

今後の展望：AI数学研究の未来

ワイルズによる証明は1995年にすでに存在していた。今回新しいのは、その議論のすべてのステップが、数年ではなく数分以内に機械によって検証可能になったという点だ。そしてその達成を可能にしたのは、形式化専門家のチームではなく、ほぼ自律的なマルチエージェントシステムだった。

このプロジェクトは、Leanが数千ページに及ぶ非形式的な数学をまたぐ非常に複雑な数学的主張を処理できることを示した。

ただし、計算コストの側面も無視できない。1プロジェクトあたり約60億の出力トークンという規模は、完全自律的な形式化の経済性がモデルの効率性、オーケストレーションの質、コンパイルインフラ、そして数学的ターゲットの価値に依存していることを示している。

今後は以下のような展開が注目される：

リーマン予想をはじめとする未解決問題へのAI適用の加速
形式化された数学ライブラリの飛躍的な拡充
医療・航空・金融などの安全クリティカル分野への形式検証技術の普及
AIエージェントを活用した自律的な科学研究プロセスの標準化
オープンソースの形式化ツールと商用AIの融合による研究民主化

まとめ：この出来事の3つのポイント

AIが358年越しの数学難問を11日間で形式証明：ClaudeはProve2Meプラットフォーム上で自律的に動作し、フェルマーの最終定理の史上初のコンピュータ検証済み完全形式証明を生成。1300万行のLeanコードと2万9500の中間定理を含む史上最大のLean証明となった。
マルチエージェント自律協調が鍵：数十のClaudeエージェントが分散・協調して証明を構築したことで、単一モデルでは不可能だった規模と複雑さを実現。オープンソースのProve2Meプラットフォームが効率的なタスク管理を支えた。
AI科学研究の新時代の幕開け：専門家が「予測より大幅に早い」と評した今回の成果は、AIが形式数学のフロンティアを押し広げる時代の到来を示しており、学術・産業・安全システム検証など幅広い分野への波及効果が期待される。

参考情報

著者プロフィール

伊東雄歩（いとうゆうほ） / ゆぽゆぽ

株式会社ウォーカー代表取締役 / MENSA会員 / NLPマスタープラクティショナー

IQ130超のADHD経営者。「社会不適合」ゆえに会社員を2年で挫折し、フリーランスを経由せずいきなり起業。訴訟4回、2000万円の損失、役員の裏切り、オフショア開発の地獄を乗り越え10年生き残る。心理学・教育学に1000万円投資し、独自の「成長力学」を確立。現在は生成AI教育に注力し、「3年を2日に変える」AIプログラミング2Daysキャンプを全国展開中。AIフレンズコミュニティを運営。

夢は「世界征服」——世界の常識を変え、新しい価値観を提示すること。