Claudeがフェルマーの最終定理を11日で機械検証　新発見ではなく既存証明の形式化

Claudeが行ったのは、フェルマーの最終定理の新発見ではありません。
人間が築いた既存証明をLean 4のコードへ置き換え、コンピューターが論理を最後まで検査できる形にした成果です。

Anthropicは2026年9月4日、クロード(Claude)が多数のエージェントに分かれて作業し、11日間で約1,300万行の証明コードを構築したと発表しました。
「Claudeが350年以上解けなかった難問を11日で解いた」と読むのは誤りであり、価値は証明の形式化と検証規模にあります。

数学ニュースとして何が新しく、機械検証がどこまで正しさを支えるのか。
見出しの数字だけでは分からない前提まで、経営者にも分かる言葉で切り分けます。

Claudeがフェルマーの最終定理を11日で機械検証した内容

Anthropicによると、Claudeはフェルマーの最終定理について、初の完全なコンピューター検証可能証明をLean 4で構築しました。
Leanは証明の文章を評価するのではなく、形式化された各推論が規則どおりにつながるかを検査する証明支援系です。

発表で確認できる主要数値

項目	公表値	読み方
作業期間	11日	プロジェクト全体
コード量	約1,300万行	Leanコード
全定理	約3万300件	生成した部品
使用定理	約2万9,500件	最終証明で使用

約1,300万行は人間向け論文の長さではなく、Leanが検査するコード量です。
行数の多さだけで賢さを測るのではなく、約2万9,500件の定理が依存関係を保ったまま最終結論へつながった点を見ます。

出典: Anthropic「Formalizing Fermat’s Last Theorem」(英語)

Claudeを開発した会社との関係から知りたい場合は、ClaudeとAnthropicの基本情報も先に押さえると、今回の発表主体を取り違えません。

フェルマーの最終定理は新発見ではなく既存証明の形式化

フェルマーの最終定理は、3以上の整数nについて、aⁿ+bⁿ=cⁿを満たす正の整数a、b、cは存在しないという命題です。
Andrew Wilesの1995年の論文と、Richard Taylorとの補完につながる仕事によって、数学上はすでに証明されています。

出典: Annals of Mathematics「Modular elliptic curves and Fermat’s Last Theorem」(英語)

公開物もゼロからの生成ではなく、Imperial College LondonのFLTプロジェクト、flt-regular、Mathlibを土台にしています。
人間の数学者、先行形式化、公開ライブラリの蓄積を消して「Claude単独の11日」と比べてはいけません。

AIの回答と原典をどう分けて読むかは、生成AIの回答に混じる誤りを裏取りする手順にも通じます。
モデルが自信ありげに説明したかではなく、外部の根拠で検査できるかを基準にしてください。

11日を支えたClaudeエージェントの分業

11日という期間を支えたのは、多数のClaudeエージェントとProve2Meという協調基盤です。
大きな証明を依存関係に沿って分け、合格した定理だけを次の仕事から参照できるようにしました。

Anthropicは約60億出力トークンを使ったと説明しており、単一のチャットが11日考え続けた話ではありません。
Prove2Me論文も、この事例は統制実験ではなく、モデルと作業基盤の効果を切り分けられないと明記しています。

出典: arXiv「Prove2Me: An Open Collaborative Platform for Scaling Math Formalization」(英語)

• 問題分割: 先に証明すべき定理と、後から使う定理を分ける
• 合否判定: Leanのエラーを根拠に修正する
• 成果の再利用: 合格済みの定理を別エージェントが参照する
• 証跡: 最終結論までの依存関係を残す

機械検証された証明はどこまで信頼できるか

機械検証された証明は、形式化した命題が、採用した公理と推論規則から導けることを強く確認します。
今回の最終証明は、Leanの標準的な3公理だけに依存し、未完成を示すsorryや追加公理を認めない構成です。

さらに公式リポジトリでは、Leanによる全体ビルド、Mathlibだけで書いた課題命題との同一性を調べるcomparator、別実装のカーネルnanodaを使っています。
同じ仕組みだけを信じない検査を重ねた点が、今回の証明の信頼性の根拠です。

出典: Anthropic公式GitHub「Fermat’s Last Theorem in Lean 4」(英語)

AI生成コードでも、書いた本人の説明だけでは合格にできません。
AIで作ったコードを納品前に検査する3点のように、成果物とは独立したテストを残す考え方が必要です。

経営者がClaudeの事例から学べる4条件

Claudeによるフェルマーの最終定理の形式化から企業が持ち帰るべきものは、数学の規模より検証可能な仕事の設計です。
AIへ長く任せたい業務では、次の4条件を先にそろえます。

• 合格条件: 正しい出力を機械または人が判定できる
• 小さな分解: 前後関係を保ったまま担当を分けられる
• 独立検査: AIの自己評価ではなく別の基準で確かめる
• 人の受入判断: 目的、意味、公開可否を最後に決める

Leanに相当する判定器がない仕事へ、11日という期間だけを移植しないでください。
モデル更新後も同じ条件で比べるなら、生成AIの品質テストを固定する方法を使い、代表業務1件の合否から始められます。

Claudeとフェルマーの最終定理でよくある質問