Anthropic は最近、自社のAIモデルが基本的な自律運用を11日間行った後、フェルマの最終定理（FLT）の最初のエンド・トゥ・エンドでコンピュータで検証されたLean形式化証明を成功させたと発表しました。この作業はAIがその定理の数学的証明を再発見したわけではなく、既存の数学的証明をLean証明アシスタントが段階的に検証できる形式に変換したものです。Leanは形式的な数学証明を記述および検証するための証明アシスタントであり、証明中の論理ステップをコンピュータで検証できます。

このプロセスにおいて、Claudeは約1300万行のLeanコードを生成し、約3.03万の定理を証明しました。そのうち約2.95万の途中定理がフェルマの最終定理の完全な証明に組み込まれました。全体の証明はLeanによって検証され、Leanの標準公理3つのみを使用しました。この作業の目的は、イギリスの数学者アンドリュー・ワイルズが1995年に完成させたフェルマの最終定理の証明を形式化することでした。フェルマの最終定理は、整数の指数nが2より大きいとき、a^n + b^n = c^nを満たす正の整数a、b、cが存在しないというものです。ワイルズの元の証明は129ページに及んでおり、公開前に何ヶ月もの人間によるチェックが行われました。

数学の形式化の難点は、人間の数学的証明が多くの論理的な導出ステップを省略しているため、Leanではすべての論理的なステップを明確に検証する必要があることです。さらに、数学者は形式化されていない多くの既存の数学的結果を引用してきましたので、完全な証明をコンピュータで検証可能な形式に変換するには多くの時間がかかります。Anthropicは以前、フェルマの最終定理の形式化作業には何年もかかるだろうと考えていました。

image.png

今回のプロジェクトは、Anthropicの研究者であるTianyi Pengによって開始されました。Claudeは単一のインテリジェントエージェントによってすべての作業を完了したわけではなく、概念の定義、中間定理の証明、そしてより複雑な命題の導出を多エージェント協働によって完了しました。プロジェクトでは、Pengとコロンビア大学の共同研究者によって開発されたProve2Meプラットフォームが使用され、証明すべき定理とその依存関係を有向無環グラフで記録し、複数のClaudeエージェントが並列で作業を行うことを可能にしました。最終的な証明は、Darmon、Diamond、Taylorが提供したワイルズの証明の簡略版に従いました。人間の研究者は主に少数の高レベルな指示を提供し、例えば特定の数学的対象や定理の優先順位を決定することなどを行いました。具体的な証明作業は主にClaudeによって完了されました。

このプロジェクトには約60億の出力トークンが消費され、Claude Fable5.1とほぼ同等の汎用的な内部研究モデルが使用されました。最終的に生成された証明の規模は、主要な数学証明ライブラリであるMathlibの5倍を超えました。Anthropicは特に、今回の成果のポイントはAIが独立して新しいフェルマの最終定理の証明を提案したわけではないことに注目しています。この定理はすでに1995年にワイルズによって証明されており、今回の作業の革新点はAIを活用して大規模に証明の形式化を自動的に行い、Leanによって最終結果をコンピュータで検証したことです。

Anthropicは、このような自動形式化技術がより多くの現代的な数学の成果に拡張されるならば、数学研究における新証明の検証にかかる人間のコストを削減できると信じています。AIが生成する数学的成果の数が増えるにつれて、人間が読むための数学証明に加えて形式化されたバージョンを提供することが、今後一般的な慣習となる可能性があります。今回のプロジェクトの完全なLean証明はGitHub上で公開されています。また、数学者のKevin Buzzardはこの証明を審査し、この自動形式化の成果がAIによる大規模な数学成果の形式化に重要な進展を示していると評価しています。