Anthropicが2026年9月4日、フェルマーの最終定理(FLT)の計算機検証済み証明を初めて完成させたと発表しました。Claudeが11日間ほぼ自律的にLeanで書き上げたもので、1,300万行のLeanコードを生成し、30,300個の定理を証明(うち29,500個を最終証明に使用)しています。ワイルズによる1995年の証明は129ページで、その検証には数か月を要しました。形式化は数学コミュニティが2024年から複数年計画で進めていた作業で、初期段階の設計書だけで86ページあります。Claudeの証明はMathlib(Leanの標準数学ライブラリ)の5倍を超える規模で、Lean標準の3つの公理のみを使用し、定理の主張がMathlibのFLTの記述と一致することも照合器で確認されました。人間からの数学的な入力は「スキームとしてのヤコビアンが優先度高そう」といった短い指示に限られています。消費した出力トークンは約60億でした。
技術的に見るべきは、失敗と成功を分けた要因です。当初の試みでは、エージェントがプロジェクトの状態を見失って協調が破綻し、その失敗分が最終証明の非定型行の約7%を占めました。転機はProve2Meという共同形式化プラットフォームの導入です。定理の主張を有向非巡回グラフ(DAG)として保持することで、各エージェントが次に何を証明すべきかを判断でき、記憶の劣化を抑えつつ並列作業が可能になりました。定理の主張と証明をファイル分離してLeanのコンパイルを高速化し、各定理に自然言語の説明を付けて検索・再利用を可能にした点も効いています。9月1日に紹介した「The Station」が指揮者なしの多エージェント環境を扱っていましたが、こちらは共有された構造化状態が協調を成立させた事例と言えます。当部門の関心に引きつけるなら、Kevin Buzzard氏の「LLMが生成した数学を厳密に検証できるようになる」という指摘が重要でしょう。AIが証明を大量生産する時代に、査読の負荷を機械検証で肩代わりできるかは知識の信頼性そのものに関わります。なお、Anthropic研究者はClaude Maxの個人プラン3つでヴィノグラードフの三素数定理を3日で形式化する小実験も行っており、適切な足場があれば消費者向け契約でも大きな定理の共同形式化が可能だとしています。証明はGitHubで公開されています。
https://www.anthropic.com/research/formalizing-fermats-last-theorem