Claude、11日間でフェルマーの最終定理をLeanで形式化
Anthropicによると、ClaudeはLeanの1,300万行を記述し、フェルマーの最終定理について初の完全なコンピュータ検証済み証明を生成した。
目次 · 11
Anthropicは9月4日、Claudeがフェルマーの最終定理について初の完全なコンピュータ検証済み証明を生成したと発表した。同社によると、数十のClaudeエージェントが11日間にわたり大部分を自律的に作業し、約1,300万行のLeanコードを生成して30,300個の定理を証明した。このうち約29,500個が最終証明に含まれている。
これは、従来の数学的な意味でフェルマーの最終定理の新たな証明を発見したものではない。Andrew WilesとRichard Taylorは、1990年代に受け入れられている人間による証明を完成させた。Claudeはその代わり、文献で確立された証明経路を、論理的な各ステップをコンピュータで検査できる形式言語へと翻訳した。
この区別は重要である。この成果はフェルマーの最終定理が真であるかについて本質的に新たな知識を加えるものではないが、これまで専門家による何年もの作業を要すると考えられていた高度な数学体系を、AIシステムが形式化できることを示している。別の形式化プロジェクトを率いるImperial College Londonの数学者Kevin Buzzardは、Anthropicのコードをコンパイルし、Comparatorの検査を実行した。彼は、この証明は検証を通過すると報告した。
一、Claudeが形式的に証明したこと
フェルマーの最終定理は、整数の指数 \(n\) が少なくとも3であるとき、正の整数 \(a\)、\(b\)、\(c\) で \(a^n+b^n=c^n\) を満たすものは存在しないと述べる。この命題は初等的だが、既知の証明は楕円曲線、モジュラー形式、ガロア表現、変形理論、代数幾何学、数論に関する高度な結果に依存している。
Anthropicのリポジトリは、最終定理をLeanの自然数上で直接表現している。その命題は正の自然数 \(a\)、\(b\)、\(c\) と \(n \geq 3\) を取り、この方程式が成立しえないことを証明する。別の最終チェックでは、この定理からMathlibに既存のフェルマーの最終定理の記述を導出する。
この議論はFrey、Serre、Ribet、Wiles、Taylor–Wilesの研究、とりわけHenri Darmon、Fred Diamond、Richard Taylorによる1995年の解説に従っている。フェルマー方程式の仮想的な解とFrey楕円曲線の関係を用い、続いてモジュラー性およびレベル降下の結果を適用して矛盾を得る。
Buzzardは、この構成における重要な詳細を指摘した。AnthropicのWilesに基づく経路は、素数の指数 \(p \geq 17\) を扱う。完全な結果には、残る場合を埋めるために、すでに形式化されていた正則素数に関する研究が組み込まれている。それでも得られたLean定理は、少なくとも3のすべての自然数指数を対象とする。
この成果物は、相当量の先行する人間の作業にも依存している。Anthropicは、Imperial CollegeのFLTプロジェクト、flt-regularプロジェクト、Mathlibの資料を改変して利用したとしている。その帰属ファイルでは、最初の2つのプロジェクト由来の資料を含むファイルが106個、Mathlibのテキストを再現するファイルが23個特定されている。したがって、この成果は既存の形式化エコシステムをAI主導で統合・拡張したものであり、先行する形式数学から独立して作成された1,300万行ではない。
二、マルチエージェントシステムが証明を管理した方法
Anthropicは当初、Claudeエージェントが個別の結果を証明できる一方、より大きなプロジェクト全体を見失うことを確認した。エージェントは作業を重複させ、完成済みの定理を効果的に再利用できず、証明が大きくなるにつれて協調を停止した。失敗した試みも、最終的な定型コード以外のコードの約7%を占めている。
成功した実行では、Columbia UniversityのTianyi Pengと共同研究者が開発したオープンな協調形式化プラットフォーム、Prove2Meを使用した。Prove2Meは、プロジェクトを定理文の有向非巡回グラフとして表現する。エージェントは未完了のノードを選択し、前提条件を証明し、グラフ内の別の場所で生成された結果を再利用できる。
このプラットフォームは、定理文とその証明も分離している。この設計により再コンパイルのコストが低減され、依存するすべての定理文を乱すことなく、証明を変更または置換できる。定理ノードに付随する自然言語の説明は、拡大するライブラリを検索し、有用な依存関係を特定する別の方法をエージェントに与える。
Claude Codeベースのマルチエージェントハーネスが、11日間の実行にわたって数十のエージェントを協調させた。人間からの数学的入力は、エージェントをJacobianへ向かわせたり、Mazurの研究に関連する定理を完成させるよう求めたりするなど、時折の高レベルな優先順位付けに限定されたと報告されている。内部ログには、根となる定理が8月18日に証明済みとして記録されていた。
Anthropicによると、この実行で消費された出力トークンはおよそ60億だった。使用されたのは、Claude Fable 5.1とおおむね同等とだけ説明される内部の汎用研究モデルであり、正確なモデルと構成は公開されていない。同社は、プロジェクトの金銭的コストや計算コストを開示していない。
完成した開発には、閲覧可能なドキュメント内に29,511の定理ページと1,450の定義モジュールが含まれる。Anthropicは、最終的な依存経路に最終的に必要とされなかった結果も含め、より広い実行全体で30,300個のコンピュータ検証可能な定理を数えている。
三、証明の検証方法
形式証明が価値を持つのは、定理文、許可される仮定、検証プロセスが管理されている場合に限られる。Anthropicのリポジトリは、プロジェクトをLean 4.33.1とMathlib 4.33.0に固定し、複数の検査層を含めている。
まず、プロジェクトはゼロからビルドされた。60,475のモジュールがLeanカーネルによって検査された。最終定理は、命題の外延性、古典的選択、公理的商の健全性という、標準Leanの公理ちょうど3つに依存している。分散された証明モジュールには、未完了のsorryプレースホルダー、新たに宣言された公理、unsafeコード、ネイティブ決定のショートカット、外部実装は含まれていない。
次に、プロジェクトはLean Comparatorを使用し、証明された定理をMathlibだけに基づく別途提供されたチャレンジ文と比較した。この検査は、解が同じ命題を証明し、未承認の公理を使用せず、カーネルに受理されることを確立するためのものだ。Comparatorは受理判定を返した。
第3に、nanodaと呼ばれる独立したLeanカーネル実装が、エクスポートされた環境のバージョンを検査し、1,052,234件の宣言をエラーなく受理した。Anthropicはnanodaに4つのパッチを適用した。1つは進捗出力のため、3つは定義的等価性の探索を高速化するためのものだ。リポジトリによると、いずれも型付け規則を変更または弱体化するものではない。
Buzzardは最も関連性の高い外部確認を提供した。彼は96コアのマシンでコードをコンパイルし、自らComparatorを実行した。リポジトリは1,340万行を超え、Leanの数学ライブラリよりコンパイルにほぼ20倍長い時間を要したと述べた。
すべての検査を再現することは可能だが、ハードウェアへの要求は大きい。Anthropicが文書化したビルドは、96並列ジョブで5時間32分を要し、メモリ使用量のピークは153 GBで、Leanビルドには約67 GB、削除可能な生成Cファイルには最大220 GBを使用した。Comparatorの実行には14時間46分を要し、ピークは230 GBだった。第2カーネル向けに環境をエクスポートすると、37.8 GBのファイルが生成された。
これらの検査は、少なくとも1つの検査カーネルと周辺の検証ツールの正しさを仮定したうえで、正確な形式的命題が列挙された公理から導かれることを確立する。ただし、各中間定理の機械生成された名前が、その数学的意味を正確に表していることを自動的に確立するわけではない。Anthropicは、主要な数学的ステップを正確なLean定理文に対応付ける証明経路文書によって、この制約に対処している。
四、AI支援数学に何が変わったのか
この成果以前、フェルマーの最終定理は、Freek Wiedijkによる長年続く100の著名な定理形式化チャレンジのリストに残る最後の項目だった。Imperial Collegeのプロジェクトは2024年に5年分の資金で始まり、当初は定理を1980年代末までに既知だった結果へと還元することを目指していた。プロジェクト資料では、完全な形式化には数千ページに及ぶ非形式的数学を翻訳する必要があると記されていた。
Anthropicの証明は、その代わりに最終定理までを端から端まで到達している。Buzzardは、これは自身のプロジェクトを冗長にするものではないと強調した。Imperialの取り組みは、再利用可能で人間が読めるMathlibへの追加を開発しており、より現代的な証明に従っている。Anthropicは自らのリポジトリを、保守されず、コントリビューションも受け付けない研究成果物と位置付けている。
したがって、実務的な進歩はスループットにある。Claudeのエージェントは、代数学、調和解析、幾何学、数論にまたがる形式的な定義と証明を、Mathlibの行数を5倍以上上回る規模で組み立てた。この成果は、グラフベースのエージェントシステムが、単一モデルのコンテキストには大きすぎる形式化にまたがって依存関係を維持し、作業を協調できることを示している。
この証明は、AI生成数学の検証経路も実証している。言語モデルは説得力のある文章で誤った自然言語の議論を生成できるが、Leanは型検査を通過しない証明項を拒否する。別個に管理された定理文とComparatorは、エージェントが問題を密かに弱めたり変更したりして成功するリスクをさらに低減する。
この仕組みは数学者の必要性をなくすものではない。形式的な命題が意図した概念を捉えているかを判断し、結果の重要性と説明を評価し、再利用可能なライブラリを維持する必要は依然として人間にある。しかし、定義、定理文、信頼された検証境界が独立して検査されるなら、論理的ステップの網羅的な検査を人間の査読者から証明支援系のカーネルへ移すことはできる。
よくある質問
Claudeはフェルマーの最終定理の新たな証明を発見したのですか？
いいえ。Leanがすべての論理的ステップを検査できるよう、Frey–Serre–Ribet–Wiles–Taylor–Wilesの文献で確立された証明経路を形式化した。
この成果は独立して検証されましたか？
Kevin Buzzardは公開コードをコンパイルし、Lean Comparatorを実行して、検証を通過すると報告した。リポジトリには、Leanと独立したnanodaカーネルによる検査成功も記録されている。
どのClaudeモデルが証明を生成したのですか？
Anthropicは正確な公開モデル名を明らかにしていない。内部の汎用研究モデルを、Claude Fable 5.1とおおむね同等と説明している。
研究者は検証を再現できますか？
はい。コードと手順はApache 2.0ライセンスの下で公開されている。完全な再現には、検証段階によって数百GBのメモリを含む相当なハードウェアが必要となる。
1,300万行のリポジトリはすべてAIが新たに記述した数学ですか？
いいえ。AIエージェントは開発の大部分を生成・統合したが、Mathlibと、Imperial College FLTおよびflt-regularプロジェクトによる先行するオープンソースの形式化作業を基盤としている。
参考ソース
Share