Claudeは11日間で「フェルマーの最終定理」をLean形式化したのか――1300万行の意味

これは「新たに解いた」話ではない

Anthropicは、Claudeがフェルマーの最終定理（FLT）の最初の完全な、エンドツーエンドでコンピュータ検証可能なLean形式化を作成したと報告している。重要なのは、ClaudeがFLTの新しい証明を発見したわけではない点だ。すでに確立された現代的な証明の道筋を、Leanが機械的に検査できる極めて大規模な成果物へ変換した、というのが主張の核心である。Anthropicによれば、作業は主に自律的なエージェントによって約11日間続き、Leanコードは約1300万行に達した。215

FLTは、自然数 (a,b,c) と (n\geq3) について、(a^n+b^n=c^n) が非自明な解を持たないという定理である。MathlibにおけるLeanの定式化では、解があれば (a=0)、(b=0)、(c=0) のいずれかでなければならない、と表現される。これは「正の整数解は存在しない」というよく知られた言い方と同値だ。31

プロジェクトは、ワイルズ／テイラー＝ワイルズによる証明戦略のうち、Darmon–Diamond–Taylorによる提示を採用した。つまり、証明の経路を新規に考案したのではない。通常の論文なら「標準的な議論から従う」と省略できる定義、仮定、補助定理、推論の接続まで、形式化では全てを明示する必要がある。インペリアル・カレッジ・ロンドンのFLT形式化プロジェクトも、ワイルズ／テイラー＝ワイルズ証明の現代的な変種を採るとしている。511

1300万行になった理由

Leanのような証明支援系では、もっともらしい自然言語の説明だけでは証明にならない。各推論を型検査できる形で書き下し、その結果が形式化済みの定義・補題・定理へと連なっていなければならない。

Anthropicの報告では、プロジェクト中に約3万300のコンピュータ検証済み定理が作られ、そのうち約2万9500が最終定理へ至る依存関係に含まれた。成果物は代数学、幾何学、調和解析、数論にまたがるという。215

したがって「11日」という数字は、FLTをめぐる長い知的営みが11日間に短縮された、という意味ではない。Anthropicは生成トークン数を約60億としており、そこには候補となる証明、Leanによる検査、エラーを受けた修正、長期間走る形式化プロジェクトを整理するための実装作業が含まれる。5

要は、1つのAIではなく「分業するAI群」

報告された成果は、単一モデルが膨大な証明全体を文脈内に保持し続けた結果ではない。Anthropicによると、初期の試行は前進した一方で、プロジェクト全体の共有状態を維持しにくかった。成功した実行では、共同数学形式化向けプラットフォームであるProve2Meを基にしたハーネスを用いたという。529

中核は、有向依存関係グラフによる仕事の管理だ。

• ノードは、未解決の定義・補題・定理を表す。
• 辺は、後続の結果に何が必要かを表す。
• エージェントは有用で未解決の課題を選び、Leanで証明し、成果を他のエージェントが使える形で残す。
• これにより、基礎部品から最終定理へ向けて段階的に進められる。

Prove2Meは、AIエージェントが再利用可能な形式証明を持ち寄る「ミッション」を立ち上げる仕組みとして説明されている。29 一続きで壊れやすい巨大タスクを、多数の検査可能な小問題へ分割し、個々のモデル実行の外部にプロジェクト記憶を作る発想だ。

「コンピュータ検証済み」は何を保証するのか

Anthropicは、最終プロジェクトには未証明のまま命題を受け入れるLeanのプレースホルダー sorry がなく、Leanの標準的な3公理のみに依拠していると説明する。5

これは、AIが自然言語で一見もっともらしい証明文を書いた、という話よりはるかに強い。Leanのカーネルは、符号化された各段階が、システムの論理規則・公理・インポートされた依存関係の下で成立するかを検査する。Anthropicはさらに、最終の主張がMathlibにある FermatLastTheorem の定式化と一致することを確認したとしている。531

ただし、検査の境界も明確だ。カーネルが検証するのは、符号化された形式命題である。形式的な定義や中間命題が、もとの非形式的な数学の意図を正確に表しているかは自動的には保証されない。公開された成果物を第三者がコンパイルできるか、依存関係を専門家が監査できるかが、今回の主張を評価する重要な試験になる。

ケビン・バザードが「並外れた」と評した理由

Anthropicの報告によれば、インペリアル・カレッジ・ロンドンの数学者ケビン・バザードはこの結果を「並外れた自動形式化の達成」と評した。21 意義は、AIエージェントが単発のLean演習を解けることだけではない。従来なら協調する人間が何年もかけると想定されていた、深く積み重なった再利用可能な形式化を組み上げた、という主張にある。

再現可能でコスト面でも実用的なものになれば、形式化には次のような可能性がある。

• 検証の厳密化：論文の文章では見落としやすい仮定漏れ、不正な変形、定義の食い違いを検出しやすくなる。
• 基盤の再利用：一度形式化した補題は別のプロジェクトでインポートでき、細部を毎回作り直さずにカーネル検証へ委ねられる。
• 査読の補完：非常に長い技術的議論の論理検証の負担を減らしつつ、数学者は意味、重要性、戦略の評価に集中できる可能性がある。

もっとも、これは数学者の判断を自動的に置き換えるという話ではない。形式証明は論理的に正しくても、そもそも意図と異なる命題を形式化している可能性は残る。また、1300万行の成果物を生むための計算資源とエンジニアリングのコストも小さくない。

今回の発表をどう読むべきか

今回のFLTの報告は、すでに証明済みの大定理を対象とし、最終成果物が独立に検査可能であることを目指している点で、AI支援による数学形式化の重要なベンチマークといえる。ただし、「Claudeがフェルマーの最終定理を新たに解決した」と表現するのは正確ではない。

最も適切な理解はこうだ。Anthropicは、依存関係グラフによるタスク分解と形式検証からのフィードバックを使い、協調したAIエージェント群が既知の大規模証明を、前例のない規模でLean開発へ変換したと報告している。21529

今後の焦点は、外部研究者がビルドを再現できるか、形式化が意図した数学を正しく表すかを監査できるか、部品を別の研究で再利用できるか、さらに他の高度な数学でも同程度の成果を得られるかにある。今回が一度きりのエンジニアリング上の偉業なのか、それとも現代数学の証明の作り方・確かめ方を変える持続的な転換なのかは、これらの検証によって決まる。