検証

Anthropic、Claudeがフェルマーの最終定理の「計算機検証済みの完全な証明」を11日で作成Leanで1,300万行、中間定理29,500本、Mathlibの5倍超。数十のエージェントがProve2Me（定理のDAG）で分担、Fable 5.1相当の社内モデルで出力約60億トークン。Buzzard氏「数学の公理以外の仮定なし」。Max 3契約で三素数定理も3日

2026年9月28日公開執筆：AI時短ラボ約7分で読めます

日刊AIニュース11月3日（火）号：前日のAIのニュース2本を短くまとめました（約4分）›

Anthropicは2026年9月4日、Claudeがフェルマーの最終定理（FLT）の初の端から端まで計算機で検証された証明を、Lean証明支援系で書いたと発表した。コロンビア大学で形式化の道具を作るTianyi Peng氏の試みで、Claudeはほぼ自律的に11日で1,300万行のLeanを書き、30,300本の定理を証明し（最終証明で29,500本を使用）、Mathlibの5倍超の規模になった。初期の試みは複数エージェントが状態を見失って協調できず失敗し、成功したのはProve2Me（定理文の有向非巡回グラフで次に取り組む証明を決め、文と証明をファイル分離、自然言語の説明で検索・再利用）に切り替えてから。Claude Codeベースのマルチエージェント構成で2週間弱、Claude Fable 5.1におおむね相当する社内研究モデルが出力約60億トークンを消費。Leanの標準3公理だけを使い、Mathlibの文と一致することを確認。Kevin Buzzard氏が査読。個人のClaude Max 3契約でヴィノグラードフの三素数定理を3日で形式化した小実験も。

Anthropic、Claudeがフェルマーの最終定理の「計算機検証済みの完全な証明」を11日で作成──Leanで1,300万行、中間定理29,500本、Mathlibの5倍超。数十のエージェントがProve2Me（定理のDAG）で分担、Fable 5.1相当の社内モデルで出力約60億トークン。Buzzard氏「数学の公理以外の仮定なし」。Max 3契約で三素数定理も3日

新しいのは証明でなく検証という点
確認は原文の数字のみ、証明は未検査
モデル名・費用換算は本文になし
出典はAnthropicの研究記事
関連記事

2026年9月18日・日本時間時点の情報です。 Anthropicの研究記事（9月4日）を読んだ。当サイトはClaudeのリーマンゼータやAstraの10本の数学証明のような「新しい数学」は追ってきたが、こちらは検証の話で、扱っていなかった。

3行まとめ

何をしたか。 1637年ごろのフェルマーの余白の主張（n>2で aⁿ＋bⁿ＝cⁿ を満たす正の整数はない）は、1995年にWilesが129ページで証明し、検証に数か月かかった。その証明を計算機が自動で検査できる形に書き直す「形式化」は、2024年にImperial College LondonのKevin Buzzard氏が始めた複数年のコミュニティ事業で、初期段階の設計書だけで86ページ、完了には年単位が見込まれていた。Anthropicの研究者でコロンビア大学に形式化の道具を作るグループを持つTianyi Peng氏が試したところ、Claudeはほぼ自律的に11日で端から端まで計算機検証済みの証明を作った。Lean 1,300万行、30,300本の定理を証明（最終証明で29,500本を使用）、Mathlib（コミュニティの証明ライブラリ）の5倍超。証明はDarmon・Diamond・TaylorによるWilesの証明の簡略版に沿い、人間の数学的入力はPeng氏の高レベルの指示（「スキームとしてのヤコビアンは優先度が高そう」「Mazurの定理を早く終わらせて」）に限られた。

どう組んだか。 最初の試みは、複数のエージェントが早い段階で成果を出しつつもプロジェクトの状態を見失って協調できなくなり失敗した（その残骸が最終証明の非定型行の約7%）。成功したのはPeng氏らのProve2Me（オープンな協働形式化プラットフォーム）に切り替えてからで、①定理文の有向非巡回グラフ（DAG）でエージェントが次に取り組む証明を決める（記憶の劣化を抑え並列化）、②定理文と証明を別ファイルにしてLeanのコンパイルを速くし資源を抑える、③各定理文の自然言語の説明を持ち検索と再利用を可能にする。Claude Codeベースのマルチエージェント構成で2週間弱、Claude Fable 5.1におおむね相当する社内の汎用研究モデルが出力約60億トークンを消費。完成した証明はLeanが検査し、Leanの標準3公理だけを使い、比較器で定理の文がMathlib自身のFLTの文と一致することを確認した。Buzzard氏の評は「数学の公理以外の仮定なしにFLTを証明している。代数・調和解析・幾何・数論の自動形式化が見え、AIの自動形式化の成果物は積み上げに耐えるほど頑健になった」。

何を意味するか。 記事は「新しい数学」（リーマン予想の仕事）と対比し、ここで新しいのは検証だと書く。AIが証明を量産する時代に、査読（年単位になり得る）の負担を形式化で軽くでき、「人が読む解説と並べて形式化された証明を付けるのが普通になる」と見る。Leanを書くことがClaude自身の仮説検証にも役立っているとも。別の小実験では、個人のClaude Max 3契約だけでProve2Meを通じて協働し、Hardy–Littlewoodの円周法の応用としてヴィノグラードフの三素数定理を3日で形式化した。証明全体と解説はGitHubで公開。

新しいのは証明でなく検証という点

「11日」は最終的に成功した走行の日数で、失敗した試みの期間は別。約60億出力トークンという費用は「トークン集約的」と本文が認めており、Max 3契約の小実験は「消費者向け契約でも大きな結果の協働形式化ができる」ことを示すための対比
中身の数学はWilesの証明を追ったもので、新しい定理を証明したわけではない。検査したのはLean（機械）で、Buzzard氏は成果物を確認した立場
Claudeの思考の抜粋（「THE FLT root reads Proved on the site. Historic moment (modulo re-check)」）が載っており、「modulo re-check」と自分で留保している
Anthropicの科学者向け支援は形式化やLean/Mathlibの改善も対象に入る、と本文が触れている

確認は原文の数字のみ、証明は未検査

この記事の下調べで、筆者は9月18日にAnthropicの研究記事を取得し、11日・1,300万行・30,300／29,500本・5倍超・約7%・約60億トークン・Prove2Meの3機能・Buzzard氏のコメント・Max 3契約で3日の記述がその原文にあることを確認した。GitHubの証明本体とProve2Meの論文（arXiv 2608.28433）は開いていない。筆者はLeanで証明を検査していない。