9月5日、Techstrong.aiが「Anthropic's Claude Agents Formalize Fermat's Last Theorem in 11 Days」と題した記事を公開した。AnthropicのClaudeエージェント群が、数百年来の難問「フェルマーの最終定理」の形式的証明を11日間で完成させたという内容だ。
Andrew Wilesが約7年かけた証明を、Claudeは11日で形式化
フェルマーの最終定理（Fermat's Last Theorem、以下FLT）とは、「$n \geq 3$ のとき、$x^n + y^n = z^n$ を満たす正の整数 $x, y, z$ は存在しない」という命題だ。1637年にフェルマーが書き残し、Andrew WilesがRichard Taylorとともに1986年から約7年をかけて研究し、1994〜1995年にようやく証明したことで知られる。
今回Anthropicが達成したのは、その「証明」ではなく「形式化（formalization）」だ。形式化とは、数学的な証明を、コンピュータが一行ずつ検証できる厳密な記述形式に翻訳する作業を指す。これは従来、極めて時間のかかる手作業で、Lean（定理証明支援系）を使ったFLTの形式化プロジェクトは、数学者のKevin Buzzard（インペリアル・カレッジ・ロンドン）が2024年からコミュニティ総がかりで取り組んでおり、完成まで数年かかると見られていた。同プロジェクトには多くの数学者が関与する大規模な共同作業として知られており、Claudeエージェント群はその規模に匹敵する作業をわずか11日で完了したことになる。
生成されたLeanコードは1,300万行、証明に使われた中間定理は3万以上に上る。
「エージェントが途中で迷子になる」問題をどう解決したか
エンジニアにとって特に興味深いのは、Anthropicがぶつかった課題とその解決策だ。
長期間動作するエージェントを開発した経験があれば思い当たるはずだが、個々のエージェントは途中で全体像を見失い、相互の連携が崩れ始めた。この問題は規模が大きくなるほど顕在化する。
Anthropicの研究者Tianyi Pengと、Columbia大学の共同研究者たちは、このために**Prove2Me**というオープンプラットフォームを開発した。Prove2Meは以下の役割を担う。
- 証明の各パーツがどの部分に依存しているかを追跡
- 複数エージェント間の作業を調整
- 完成済みの結果を再利用しやすい形で管理
このProve2MeとClaude Codeベースのマルチエージェントワークフローを組み合わせ、数十のエージェントが証明の異なるパートを並列に処理する構成を実現した。
消費トークン数は約60億出力トークン。使用モデルは、Anthropicの社内汎用リサーチモデルだ。
証明の信頼性をどう担保したか
Anthropicは形式化の完全性についても明確な基準を示している。
- Leanの標準的な3つの公理のみを使用
- 未完成ステップのプレースホルダーや、議論を成立させるための追加公理は一切含まない
- Mathlibの既存FLT命題との照合を実施
- 第二の独立したLeanカーネル実装による検証も通過
完成したコードはGitHub上で公開されており、BuzzardはこれをAI「extraordinary autoformalization achievement（驚異的な自動形式化の成果）」と評した上で、代数、調和解析、幾何学、数論にまたがる作業をAIが形式化し、今後の数学研究の土台となりうる形で残したことを認めた。
次のターゲットはリーマン予想
先月（8月）、Anthropicは未公開のClaudeモデルを用いてリーマン予想に関連する問題に対しても同様の形式化プロセスを適用した。リーマン予想はミレニアム懸賞問題の一つで、解決には100万ドルの賞金がかかっている。元記事では、リーマン予想そのものではなく関連する問題への形式化アプローチが紹介されており、今後の展開が注目される。
Anthropicは今後に向けて、外部の数学者が形式化プロジェクトに取り組む際の無償・割引アクセス、研究クレジット、グラントの提供も拡充している。同社は公式ブログで「形式化がより一般的なツールになれば、数学的知識の共有資産への信頼を維持する助けになる」と述べている。
詳細はAnthropic's Claude Agents Formalize Fermat's Last Theorem in 11 Daysを参照していただきたい。
