この記事のポイント
- Claudeはワイルズの証明をLeanで機械検証できる形に形式化しました。定理を新たに発見した成果ではありません。
- 複数エージェントが11日で1,300万行のLeanコードと中間定理を作成しました。
- Leanが論理を検証しても、人が読める説明の代わりにはならないとAnthropicは述べています。
Anthropicの発表をもとに、フェルマーの最終定理の証明をLeanで形式化した研究を紹介します。AIが新しい証明を発見したのではなく、既存の証明を機械検証可能にした点が中心です。
新しい証明ではなく、既存の証明を機械検証可能に
フェルマーの最終定理は、数学者アンドリュー・ワイルズ氏が1995年に証明したことで知られる有名な定理です。今回の発表は、この証明を新たに考え出したのではなく、ワイルズ氏の証明を整理したDarmon・Diamond・Taylor版に沿って、コンピュータが機械的にチェックできる形に書き直した(形式化した)という成果です。ひとことで言うと、証明をLean(リーン)という証明支援言語のコードで表現し、論理の矛盾の有無をコンピュータが検証できるようにしたということです。
公式発表によると、Claudeの内部研究モデル(性能は「Claude Fable 5.1」相当)が複数のエージェントで協調し、約1,300万行のLeanコード・3万300個の定理(うち2万9,500個を最終証明で使用)を、11日間・約60億の出力トークンで生成したとのことです。詳細は一次情報のAnthropic公式ブログ「Formalizing Fermat’s Last Theorem」にまとまっています。
定理の依存関係を管理する協調基盤
鍵になったのが、コロンビア大学の研究者らが開発した協調プラットフォーム「Prove2Me」です。公式発表によれば、証明すべき定理どうしの依存関係を有向グラフで管理し、複数のAIエージェントが同時並行で作業しても手が重ならないよう采配したとされています。
1体のAIが黙々と書き続けたのではなく、大量のエージェントが役割分担して並行作業できる「現場」を整えたことが、期間短縮の大きな要因だったといえそうです。エージェントを協調させる発想は、以前ご紹介したAIが実験ロボットを自分で操作できる新規格「Model Hardware Standard」とも通じます。
機械検証と、人が読む証明の役割
数学の世界には「新しい証明が発表されても専門家のチェックに何年もかかる」という悩みがあります。著名な数学者ケビン・バザード氏は今回の成果を「11日でこれほど大がかりな自動形式化ができたのは驚異的で、数学の公理以外を前提にすることなく証明している」と評し、「現代数学の文献全体を自動で形式化する道に近づいた」とも述べています。同発表では、Claude Maxプラン3契約分だけで別の定理(ヴィノグラードフの三素数定理)を3日間で形式化できた実験も紹介されています。
今回使われたのは一般提供のClaudeとは異なる内部研究モデルで、発表ではClaude Fable 5.1相当の性能と説明されています。
まとめ: 協調作業を支える検証方法を決める
形式検証や研究支援に関わる方は、作業をどう分割し、各段階をどう検証するかに注目するとよいでしょう。今回の内部研究モデルの成果は、一般提供モデルで同じ作業を再現できる証拠ではありません。Leanによる論理検証と、人が読める説明の両方が必要です。
※ この記事は2026年9月時点の情報をもとに執筆しています。AI研究の進展は速いため、最新情報はAnthropic公式発表を確認するとよいでしょう。
