Anthropicは、Claudeがフェルマーの最終定理の最初の完全な形式的証明を完了したと発表しました。これはこの定理の再発見ではなく、既存の証明をコンピューターが行ごとに検証可能な論理コードに転写したものです。同社によると、この作業には11日かかり、最終的に約1300万行の内容が生成されました。
形式化証明の意義は、数学的議論を機械が検査可能な言語で記述することにある。従来の論文による証明は、同行審査に長期間を要し、途中のいずれかのステップに欠陥がある場合、修正に数ヶ月から数年かかることもある。フェルマーの最終定理は1995年にイギリスの数学者アンドリュー・ワイルズによって証明されたが、その証明を完全に機械検証可能な形式に変換することは、依然として高強度のエンジニアリング作業と見なされている。
11日で長期プロジェクトの目標を達成
ロンドン帝国理工学院の数学者ケビン・バズァードは、2024年から、ウィールズの証明をLean証明支援ツールに転写することを目的としたプロジェクトを推進している。当初の計画では、この作業は長期的な協力が必要であり、資金は2029年まで確保されている。
Anthropicは、Claudeがこのタスクで同類の目標を前倒しで達成したと述べている。Buzzardがレビューした結果、この証明は追加の仮定に依存せずに、数学の最も基本的な公理系のみに基づいて成立することが確認された。
複数エージェントが並列で完了
Anthropicによると、コロンビア大学の研究者Tianyi Pengチームは、複数のClaudeエージェントを並列で動作させ、それぞれが定義の作成や小さな結論の証明を担当し、段階的に大きな証明構造を組み立てました。人間の介入は最小限で、主に段階的な優先順序を提示するだけでした。
初期の進展は順調ではなかった。Anthropicは、一部のエージェントが完了した内容を共有できず、作業が重複する問題が発生したと述べている。その後、チームはProve2Meというツールを導入し、各エージェントに統一されたタスクリストとファイルの整理方法を提供するとともに、自然言語でのメモを残して、エージェント同士の結果の再利用を可能にした。
- サポート定理が3万以上
- 総消費量が数十億トークンに達しました
- 最終的に約1300万行を証明しました
新しい定理ではなく、検証可能性に重点を置く
今回の成果の重点は、新たな数学的命題を発見することではなく、既存の重要な証明をコンピューターが段階的に検証可能な形式に変換することにあります。数学論文やAI生成コンテンツの増加に伴い、人間が証明を一つずつ検証するコストも上昇しており、そのため形式化ツールへの関心が高まっています。
Anthropicは、この証明の規模が数学界で一般的に使用される共有ライブラリMathlibの5倍以上であると述べました。完全なファイルはGitHubにアップロードされ、研究者はその構造と正確性を一行ずつ検証し続けることができます。