Last Updated on 2026年9月6日 by oba3
アンソロピック（Anthropic）は2026年9月4日、クロード（Claude）がフェルマーの最終定理について、最初の完全なコンピューター検証済み形式証明を作成したと発表した。作業期間は11日間で、生成されたリーン（Lean）のコードは約1300万行に達した。今回重要なのは、AIが350年以上解けなかった数学問題を新しく解いたという話ではない。すでに知られている証明を、コンピューターが一つ一つ検証できる形式へ変換する巨大な作業をAIエージェントがほぼ自律的に進めたことで、人間中心だった形式検証のコスト構造が変わり始めた点にある。
何が起きたのか？
アンソロピックによると、複数のクロードエージェントが協調し、11日間でフェルマーの最終定理のエンドツーエンドな形式証明を完成させた。作業中には3万300件の定理をコンピューター検証可能な形で証明し、そのうち約2万9500件が最終的な証明に利用された。
証明はアンドリュー・ワイルズによる数学的成果を基礎とし、アンリ・ダルモン、フレッド・ダイヤモンド、リチャード・テイラーによる簡略化された解説に沿って構築された。つまりクロードがフェルマーの最終定理に新しい数学的解法を発見したわけではなく、既存の数学をリーン上で厳密に再構成した。
人間の関与も完全にゼロではない。アンソロピック研究者のティエンイー・ペン（Tianyi Peng）が時折、高水準の優先順位を指示した。一方、個々の補助定理の構築や証明の接続は多数のAIエージェントが担った。全体では約60億の出力トークンを使用したとされる。
完成した証明はリーンのカーネルで検証され、別の比較ツールや独立したカーネル実装でも確認された。アンソロピックは証明データも公開しており、第三者が検証可能な研究成果として提供している。
なぜ重要なのか？
形式証明では、人間向けの数学論文で省略できるような小さな論理ステップも、コンピューターが確認できる形ですべて記述する必要がある。そのため数学的には既知の証明でも、形式化には大量の作業が必要になる。
フェルマーの最終定理についても、数学コミュニティでは形式化に数年を要すると見込まれていた。2024年からはインペリアル・カレッジ・ロンドンを中心に長期プロジェクトが進められていたが、今回クロードは既存成果も利用しながら11日間で全体を接続した。
ここで変わったのは数学的真理そのものではない。人間が長期間かけて定義を書き、補助定理を証明し、依存関係を整理していた工程を、多数のAIが並列処理できることが示された点に価値がある。
市場構造への影響
形式検証は数学だけの技術ではない。ソフトウェア、暗号技術、スマートコントラクト、航空宇宙、半導体など、間違いのコストが大きい分野でも利用される。ただし従来は、仕様を形式言語へ変換し、証明を書く専門人材のコストが普及の壁になってきた。
AIがこの作業の大部分を自動化できれば、形式検証を導入できる対象が広がる可能性がある。これまでは重要度の高い一部システムだけに投入していた検証コストを、より多くのソフトウェアやプロトコルへ振り向けられるためだ。
今回の成功では、AIモデル単体だけでなく、プルーブ・トゥー・ミー（Prove2Me）という協調基盤も重要だった。多数のエージェントがどの定理を証明済みか、次に何を処理すべきかを共有することで、長大なプロジェクトを分割して並列に進めた。大規模検証では、AIの推論能力と作業状態を管理するインフラの組み合わせが重要になることも示している。
資金・規制・流動性との関係
金融やWeb3では、形式検証のコスト低下が直接的な意味を持つ。スマートコントラクトや暗号プロトコルでは、コード上の一つの欠陥が大規模な資産流出につながる場合がある。それでも、すべてのコードを数学的に検証するには高い専門性と時間が必要だった。
AIが仕様から補助定理を作り、証明候補を大量に生成し、証明支援系が正しさを機械的に確認する流れが実用化すれば、人間のレビューだけに依存する現在の開発工程を補完できる可能性がある。
ただしAIが生成した証明だから正しいのではない。今回信頼性を支えているのは、最終成果をリーンの検証器がチェックできることだ。AIは作業を高速化する主体であり、正しさを保証する最終地点は独立した形式検証システムに残る。この役割分担が重要になる。
初心者向け補足
形式証明とは、数学の証明をコンピューターが一行ずつ論理的に確認できる形へ書き直したものだ。通常の数学論文では専門家なら分かる部分を省略できるが、形式証明ではその省略を埋める必要がある。
今回使われたリーンは、そのための証明支援システムの一つだ。クロードが1300万行を書いたとしても、リーンが無条件で内容を信じるわけではない。論理規則に違反した部分があれば検証を通過しない。
そのため今回の成果は「AIがフェルマーの最終定理を初めて解いた」のではなく、「既知の証明をコンピューターが完全に検査できる形へ大規模に変換した」と理解する方が正確だ。
Web3Timesの視点
今回見るべきなのは1300万行という巨大さそのものではない。人間が何年もかけると考えられていた形式化作業を、多数のAIエージェントが11日間で並列処理したことが重要だ。
AIが新しいアイデアを生み出す能力とは別に、既存の理論やコードを厳密な形式へ落とし込み、機械検証へ持っていく能力にも大きな経済価値がある。数学者やエンジニアの時間を大量に消費していた検証工程を自動化できれば、これまで費用面で形式検証を採用できなかった領域まで対象が広がる。
特にWeb3では、スマートコントラクトやブリッジ、暗号ライブラリなど、コードと資産移転が直結する。AIが証明作成を担当し、独立した検証器が正しさを判定する構成が成熟すれば、開発速度と検証強度を同時に高める新しい開発工程へ発展する余地がある。
今後見るべきなのはAIが次にどの難問を形式化するかだけではない。同じ手法をソフトウェア検証へどこまで転用できるか、1300万行という冗長な成果をどこまで効率化できるか、そして人間が作った仕様自体の誤りを誰が検証するかだ。今回の成果は数学者の代替というより、形式検証という高コストな専門作業を大量処理できる新しい計算基盤が現れ始めた事例として読む必要がある。
