Claude、マルチエージェント協調でフェルマーの最終定理をLean形式化、1,300万行の証明を公開

Anthropicは、Lean 4で記述したフェルマーの最終定理の形式化証明一式を公開した。[技術レポート](https://www.anthropic.com/research/formalizing-fermats-last-theorem)によると、数十のClaudeエージェントがClaude Codeのマルチエージェント・フレームワークを通じて11日間作業し、約1,300万行のLeanコードを生成。30,300件の中間定理を証明し、最終的にそのうち約29,500件を使用した。推論モデルには、能力がClaude Fable 5.1とほぼ同等の社内研究版が使われ、プロジェクト全体で約60億個の出力tokenを消費した。

初期の試みは、エージェントが次第にプロジェクトの状態を見失い、成果を効率的に再利用できなくなったため失敗した。そこでチームはProve2Meを採用し、目標を有向非巡回グラフ（DAG）へ分解した。エージェントは未完了の定理を選択して既存の成果を検索できるほか、定理の宣言と証明を別ファイルとしてコンパイルすることで、1つのノードを変更するたびに証明ツリー全体を再処理する事態を回避できる。[Prove2Meの論文](https://arxiv.org/abs/2608.28433)では、このアーキテクチャを人間とエージェントの双方が参加できる協調型の形式化プラットフォームと位置づけている。

公開された[証明リポジトリ](https://github.com/anthropics/fermats-last-theorem)では、Lean 4.33.1とMathlib 4.33.0を固定して使用し、`sorry`、公理の追加、`unsafe`などの回避手段を禁止している。Leanカーネルによる完全ビルドの後、`comparator`が最終命題がMathlib版と同一であることを再確認した。さらに、Rustで実装された別のカーネルnanodaも、105万件を超える宣言を検査した。この証明が依存するのは、Leanの3つの標準公理のみである。

これはClaudeがフェルマーの最終定理の新たな証明法を発見したということではなく、Frey、Serre、Ribet、Wiles、Taylor–Wilesによる道筋を、機械検証可能な成果物へ変換したものだ。再現コストも低くない。公式の完全ビルドでは153 GBのメモリが使用された例があり、`comparator`には約15時間を要し、ピーク時のメモリ使用量は230 GBに達した。カーネルによる検査は型の正しさを保証できる一方、中間定理の名称が数学的意味を忠実に表現しているかどうかまでは判断できない。今後は、独立したチームがこの結果を再構築できるか、また、このオーケストレーション手法がより少ないtokenと人間によるプロンプトで、ほかの大規模な数学文献も処理できるかが注目される。