［ニュース解説］Claudeがフェルマーの最終定理を11日で形式化——1,300万行のLeanコードが意味するもの

2026-09-06

はじめに

　Anthropicが2026年9月4日、フェルマーの最終定理（FLT）の完全な機械検証済み証明を公開しました。Claudeが11日間ほぼ自律的に作業し、Lean言語で1,300万行のコードを書き上げたとされています。本稿では、この形式化がどのように行われ、数学研究に何を意味するのかを解説します。

参考記事

メイン記事:

タイトル: Formalizing Fermat’s Last Theorem
発行元: Anthropic
発行日: 2026年9月4日
URL: https://www.anthropic.com/research/formalizing-fermats-last-theorem

要点

Claudeは11日間ほぼ自律的に作業し、フェルマーの最終定理の初のエンドツーエンドな機械検証済み証明をLeanで完成させた
生成されたLeanコードは1,300万行、証明された中間定理は30,300個（うち29,500個を最終証明に使用）である
成功の鍵は、コロンビア大学のTianyi Peng氏らが設計した共同形式化プラットフォーム「Prove2Me」の導入であった
証明を検証したImperial College Londonのケビン・バザード氏は、現代数学文献の自動形式化に向けた大きな一歩だと評価している
一方でバザード氏は、この成果が新しい数学を生んだわけではなく、意義は自動形式化の実現可能性にあると指摘している

詳細解説

350年の難問と「検証」という課題

　1637年ごろ、ピエール・ド・フェルマーはディオファントスの『算術』の余白に、n > 2 のとき aⁿ + bⁿ = cⁿ を満たす正の整数 a, b, c は存在しない、と書き残しました。この主張が証明されたのは358年後の1995年、アンドリュー・ワイルズ氏によってです。Anthropicによれば、その証明は129ページに及び、検証には数か月の緻密な作業が必要でした。

　ここで問題になるのが「検証」の負荷です。数学の証明は論理の連鎖であり、どこか一箇所が壊れていれば、それ以降がすべて崩れる可能性があります。実際、1993年にワイルズ氏が最初に発表した証明では、検証開始から2か月後に査読者の質問が決定的な欠落を露呈させ、修復には1年を要しました。

　こうした検証コストは、AIが数学的主張を生み出す時代にはさらに重くなると考えられます。今回の発表は、Claudeがリーマン予想の関連問題で新しい結果を出した事例とは性格が異なり、新しい数学を作ることではなく、既存の証明を機械が読める形に翻訳することに焦点があります。

11日間で1,300万行——形式化の中身

　形式化とは、人間向けに書かれた証明を、Leanのような証明支援系が機械的に検証できる形式へ書き直す作業を指します。人間向けの証明は自明な手順を省略しますが、Leanはすべての手順を明示的に要求します。そのため、FLTの形式化には数年を要すると見込まれていました。数学コミュニティが初期段階の設計図として用いてきた文書だけで86ページに及びます。

　Anthropicによれば、Claudeはこれを11日で完了し、途中で30,300個の定理を機械検証可能な形で証明しました（最終証明に使われたのは29,500個）。1,300万行というLeanコードの規模は、この定理が依拠するコミュニティの標準ライブラリMathlibの5倍を超えます。人間からの数学的な入力は、「スキームとしてのヤコビアンは優先度が高そうだ」といった高レベルの指示に限られていたとされています。

　用いられたのはダルモン・ダイアモンド・テイラーによる簡略版の証明経路です。バザード氏の解説によれば、この構成のため証明は指数 p ≥ 17 に限られますが、それ未満の正則素数についてのFLTは別プロジェクトで既に形式化されており、最小の非正則素数が37であることから全体としては埋まっているとされています。

Prove2Meが解いたのは「協働」の問題

　興味深いのは、最初の試みが失敗している点です。Anthropicによれば、初期のエージェント群は一定の成果を上げたものの、プロジェクトの状態を見失い、効果的に協働できなくなりました。その失敗分は最終的な証明のうち、定型的でない行の約7%に寄与するにとどまっています。

　転機となったのが、Peng氏らがコロンビア大学で設計した共同形式化プラットフォーム Prove2Me の導入です。Prove2Meは定理の主張を有向非巡回グラフ（DAG）として保持し、エージェントが次に取り組むべき証明を判断できるようにしました。また、定理の主張と証明を別ファイルに分離してコンパイルを高速化し、各定理に自然言語の説明を付けることで検索と再利用を可能にしています。

　この設計は、記憶の劣化を緩和し、複数エージェントの並列作業を成立させるためのものだと説明されています。単体の能力ではなく、多数のエージェントが状態を共有し続けるための足場が成果を分けたという点は、AIエージェントを業務に組み込む際にも参考になる観点だと思います。最終的な構成はClaude Codeベースのマルチエージェントで、約60億トークンの出力を消費し、Claude Fable 5.1におおむね相当する社内の汎用研究モデルが用いられたとされています。

査読者の評価と、残された課題

　証明を検証したバザード氏は、数学の公理以外の仮定を置かずにFLTを証明した成果であり、代数・調和解析・幾何・数論にわたる自動形式化が確認できると述べています。同氏はさらに、これは現代数学文献の自動形式化に向けた大きな一歩であり、こうした技術は既存の数学的知見の誤りを洗い出し、査読者の負担を軽くすると指摘しています。

　ただし同氏は、数学的にはこの成果が新しいことをほとんど示していないとも述べています。FLTの証明が正しいことは数論コミュニティでほぼ疑われておらず、形式化は初期の文献を忠実に追ったにすぎないという評価です。意義があるのは、数千ページ規模の文献が11日で形式化できると分かった点にあります。同氏はコードベースをcomparator（証明が意図した命題を証明しているか照合するツール）で検証したうえ、証明支援系の抜け穴を突いていないかを人手でも点検したと説明しています。

　一方で課題も残ります。Anthropic自身が、この証明は必要以上に長い可能性が高いと注記しています。バザード氏によれば、コンパイルには96コアの計算機でもMathlibの20倍近い時間がかかり、人間が現代的な証明を読み解くための文書化は別途必要です。Mathlibが現状ではAIによるレビューを受け付けておらず、レビュアーの時間が大きなボトルネックになっている点も、今後の統合を考えるうえで無視できない要素だと考えられます。