Anthropicは2026年9月4日、Claudeがフェルマー最終定理をLeanで形式化し、完全なコンピューター検証可能な証明を作成したと発表しました。OpenAIも9月8日、ナビエ–ストークス問題について、有限時間で特異点が生じることを示す解決案とLean形式化を公表しています。
企業のIT・研究責任者が見るべき点は、AIが一度の質問に答えたことではありません。複数のエージェントが数日間動き、途中の定理や証明を共有し、最後に機械が再検査できる成果物へまとめたことです。長時間の自律作業を業務へ持ち込むとき、作業の分割と検証の設計が成否を左右します。
ただし、2つの成果は同じ意味で「AIが数学を解いた」とは扱えません。フェルマー最終定理は既知の証明を機械検証可能な形にした形式化で、ナビエ–ストークスは未解決問題への解決案です。さらに、Leanが検査したことと、専門家や制度が解決を受け入れることも別の段階です。
※本記事は2026年10月14日時点の情報です。
AIシステム開発の種類・工程・費用・会社選定までの全体像については、無料ホワイトペーパー「AIシステム開発の完全ガイドブック」で詳しく解説しています。
フェルマー最終定理｜AIの成果は「発見」より形式化
フェルマー最終定理は、正の整数 a、b、c について、n > 2 のとき aⁿ + bⁿ = cⁿ を満たす組がないという主張です。Andrew Wilesによる最初の完全な証明は1995年に発表されており、今回のニュースで数学上の結論そのものが初めて得られたわけではありません。
Anthropicが発表したのは、その既知の証明をLeanが読める形へ書き換え、コンピューターで論理のつながりを検査できるようにする作業です。人間向けの証明では省略される細かな手順も、Leanでは一つずつ記述して確認します。成果の新しさは、数学的な発見というより、長大な証明を再検査可能な形式に変えた点にあります。
Claudeは「largely autonomously」に11日間作業し、途中で30,300個の定理をコンピューター検証しました。最終証明で使われたのは29,500個です。Anthropicは、Wilesの証明をもとにした形式化が当初は数年かかると見込まれていたと説明しています。
ポイント
フェルマー最終定理の事例は、新しい定理を発見した例ではなく、既知の証明を機械検証可能な成果物へ変換した例です。AIの数学成果は、発見と形式化を分けて評価します。
1,300万行を動かした仕組み｜共有状態と依存関係の管理
形式化の規模は、約1,300万行のLeanコードに達しました。数十のClaudeエージェントが概念の定義、中間定理の証明、最終定理の証明を分担し、出力トークンは約60億です。単一のエージェントが最初から最後まで一つの文脈で書いた成果物ではありません。
初期の試行では、エージェントがプロジェクトの状態を見失い、協調が止まりました。成功につながったのが、数学の形式化を協働で進める基盤Prove2Meです。エージェントが「次にどの証明へ進むか」を判断できるよう、定理の依存関係をDAGで管理しました。
さらに、定理文と証明を別ファイルに分け、両者のリンクを独立して管理しました。定理の自然言語による説明も検索・再利用できるようにしています。成果物を細かく保存し、別のエージェントが前の仕事を使える状態にしたことが、長時間作業の復帰と並列化を支えました。
この構造は、AIエージェントを複数使う一般の開発にも通じます。状態を共有しないまま作業を増やすと、同じ調査を繰り返したり、前提の異なる成果を統合できなくなったりします。複数エージェントの協調失敗を防ぐ設計については、マルチエージェントAIの落とし穴も参考になります。
- 依存関係：先に証明すべき定理と、後続の定理をDAGで追跡する
- 成果物の境界：定理文と証明を分け、片方だけでも再利用できるようにする
- 検索性：自然言語の説明を残し、過去の成果を次の作業から探せるようにする
ポイント
長時間の自律作業では、モデルの性能だけでなく、共有状態・依存関係・成果物の再利用・失敗からの復帰を先に設計します。
ナビエ–ストークス｜未解決問題への解決案をAIが公表
ナビエ–ストークス問題は、3次元の流体について解が存在し、滑らかさを保つのかを問うミレニアム懸賞問題です。OpenAIは2026年9月8日、内部システムが、流体に有限時間で特異点が生じることを示す解析的証明とLean形式化を作成したと発表しました。公式定式化の「C」（および「D」）を示す成果だと説明しています。
OpenAIの説明では、最初のエージェントが起動してから解決案に到達するまで約88時間かかり、Lean形式化と検証に追加で17時間を要しました。ナビエ–ストークスに取り組む過程で、エージェントは270万メッセージを送り、約1,300億の出力トークンを使っています。エージェント群の中間結果はCodexで統合しました。
ここでフェルマーの事例との違いが明確になります。フェルマーはすでに知られた証明を形式化する仕事でしたが、ナビエ–ストークスは未解決問題への新しい解決案を掲げています。Lean形式化があることは検証の入口になりますが、発表だけで数学界の最終的な受容まで完了したことにはなりません。
| 観点 | AnthropicのFLT | OpenAIのナビエ–ストークス |
|---|---|---|
| 発表日 | 2026年9月4日 | 2026年9月8日 |
| 成果の性質 | 既知の証明のLean形式化 | 未解決問題への解決案とLean形式化 |
| 作業規模 | 11日、約1,300万行、約60億出力トークン | 約88時間＋Lean検証17時間、約1,300億出力トークン |
| 外部の位置づけ | Buzzardがコンパイルとcomparator通過を報告 | Clayは「apparently settled」とし審査条件を維持 |
| 実務上の読み方 | 機械検証可能な成果物の作り方 | 新規主張を受け入れるまでの検証プロセス |
ポイント
既知の証明の形式化と、未解決問題への解決案は、成果物も受け入れ基準も異なります。AIの発表を読むときは、両者を同じ「証明」として扱わないことが出発点です。
何をもって「解決」と呼ぶか｜Lean検証と専門家受容を分ける
Anthropicの公開リポジトリには、sorry 0件、追加公理なし、使用した公理は propext、Classical.choice、Quot.sound という検査結果が記載されています。Kevin Buzzardも、リポジトリをコンパイルし、comparatorを実行してチェックが通ったと報告しました。
ただし、機械検証は万能の受け入れ判定ではありません。Leanが確認するのは、形式化された定理文と証明の論理です。その定理文が意図した問題と一致するか、途中の数学的主張が何を意味するかは、人間が読む必要があります。公開リポジトリ自身も、各中間定理の意味は読者が判断するものだと説明しています。
ナビエ–ストークスについて、Clay Mathematics Instituteは2026年9月11日、問題が「apparently been settled」と紹介し、分析と検証を急がず、今後更新すると説明しました。さらに公式ルールでは、適格な媒体での出版、出版から少なくとも2年の経過、数学界での一般的受容という3条件を満たすまで、解決案を検討しません。
OpenAIの公式ページには9月10日付の更新もあります。同時期に話題になった研究は強制Euler問題の解決で、OpenAIのナビエ–ストークス結果とは異なること、公開前に相手の成果を見ておらず、ユーザー入力が結果に影響しなかったとする調査結果が追記されました。成果の優先順位や影響経路まで含め、発表後の更新を確認する必要があります。
- 定理文：検査された命題が、元の問題の意図と一致しているか
- 再現性：公開コードを同じ環境でビルドし、検査結果を再現できるか
- 独立性：別のチェッカーや専門家が、同じ結論を確認しているか
- 受容：出版とレビューを経て、関係する専門家が成果を受け入れているか
こうした確認項目は、AIエージェントを業務へ導入するときの評価表にも置き換えられます。状態・ログ・評価を継続して見る運用は、AgentOpsの可観測性・評価・監視として整理できます。
ポイント
「コードが検査を通る」「主張が意図した定理と一致する」「専門家や制度が受け入れる」は別の確認項目です。AIの成果を採用する基準も、この3段階を分けて設計します。
企業の研究・開発に応用するなら｜形式仕様と停止条件を先に置く
フェルマーとナビエ–ストークスの事例から、企業がそのまま大規模な自律実行を始める必要はありません。むしろ、仕様を形式化でき、途中成果を保存でき、機械または独立担当者が検査できる案件を選ぶことが先です。Prove2Meの定理文と証明の分離や、OpenAIのCodexによる中間結果の統合は、その設計を考える材料になります。
最初の対象は、完了条件を文章とテストで明確に書ける小さな検証案件が向きます。エージェントに調査や実装を任せる場合も、成果物を一つの回答に閉じ込めず、前提、途中の判断、検査ログ、最終結果を分けて保存します。
- 仕様：AIが扱う対象と、完了とみなす条件を先に定義する
- 中間成果：調査、設計、実装、検査を分けて保存し、再開できるようにする
- 独立チェッカー：AI自身の自己評価とは別に、テストや担当者レビューを置く
- 停止条件：コスト上限、時間、失敗回数、要レビューの条件を決める
監督役を置かずにAIへ丸投げすると、成果物の正しさを判断できないまま作業量だけが増えます。導入時の監督体制は、AIエージェント実験の失敗事例で扱われている論点とも重なります。小さく試し、検証の証拠が残る運用だけを次の案件へ広げるのが現実的です。
ポイント
企業で始めるなら、形式仕様を書ける小さな案件から着手し、途中成果・独立チェッカー・レビュー担当・コスト上限・停止条件を一体で設計します。
よくある質問
Q. AIはフェルマーの最終定理を新しく証明したのですか？
いいえ。フェルマー最終定理はWilesらが1995年に証明済みで、Anthropicの成果はその数学的ルートをLeanで機械検証可能にした形式化です。
Q. ナビエ–ストークス問題は正式に解決しましたか？
OpenAIは解決案を発表し、Clayは「apparently settled」と紹介していますが、賞のルール上は出版後2年と数学界での一般的受容などの条件があります。
Q. Leanで検証できれば人間のレビューは不要ですか？
いいえ。Leanは形式化された定理文と証明の論理を検査します。定理文が意図した問題と一致するか、成果が何を意味するか、専門家が受容するかは別に確認します。
Q. 企業は長時間自律型のAIをどこから使うべきですか？
仕様を明確に書け、途中成果を保存でき、機械または独立担当者が検査できる小さな研究・開発案件から始めます。
まとめ
Anthropicのフェルマー最終定理は、既知の証明を11日間でLeanへ形式化し、約1,300万行のコードと多数の中間定理を機械検証した成果です。OpenAIのナビエ–ストークスは、未解決問題への解決案とLean形式化を公表した成果で、Clayは「apparently settled」としながら検証を続けています。
企業が学ぶべきなのは、AIに難問を丸投げする方法ではありません。定理文や仕様を明確にし、共有状態と中間成果を管理し、独立チェッカーと人間レビューを組み合わせる方法です。発表の大きさではなく、再現できる証拠と停止条件を基準に導入範囲を決めます。
ポイント
AIの数学成果は、発見・形式化・機械検証・専門家受容を分けて読み解きます。この区別をそのまま、企業のAI導入における仕様・検証・レビュー・停止の基準へ置き換えます。
関連記事
- マルチエージェントAIの落とし穴を解説｜Anthropic研究に見る協調失敗の教訓
- AgentOpsを解説｜AIエージェントの可観測性・評価・監視のポイント
- AIエージェント実験の失敗事例を解説｜丸投げを防ぐ監督体制のポイント
- AIがAIを作る時代をどう測るか？AnthropicのR&D自動化・監督・計算資源の指標
- AIエージェント導入を解説｜過度な期待を避けるROI評価のポイント
▼開発を相談する前に読みたい無料ホワイトペーパー
・AIシステム開発の完全ガイドブック
・【2026年最新版】AI駆動開発の完全ガイドブック
会社紹介
株式会社riplaでは、お客様の事業・ユーザー・業務に最適化したオーダーメイド型システムを、構想策定・要件定義から開発・改善まで一気通貫で支援。事業会社でIT・DXを経験したプロフェッショナルによる高い要件定義力・システム設計力を活かし、事業成果の最大化に伴走します。
また、当社独自の開発テンプレート「Boxシリーズ」による標準機能の高速開発と、AI駆動開発の独自フレームワーク「GoDD」による独自機能のAI実装を組み合わせることで、低コスト・短期間で開発を実現いたします。
もし、システム開発やプロダクト開発に関するご要望がございましたら、お気軽にお問い合わせください。
・サービス概要資料のURLはこちら >>>
・お問合せページのURLはこちら >>>
・お役立ち資料のURLはこちら >>>
株式会社ripla 代表取締役CEOとして、システムパッケージ活用、システム開発、データ分析、生成AI活用、SaaS開発、アプリ開発、EC構築など、幅広い領域で企業のDX推進と事業成長を支援している。事業会社でIT・DXを経験したプロフェッショナルが集う株式会社riplaにおいて、お客様の事業・ユーザー・業務に最適化したオーダーメイド型システムを構想策定・要件定義から開発・改善まで一気通貫で支援し、単なるシステム納品にとどまらず、クライアントと同じ目線で事業成果の最大化に向けた伴走支援を行う。早稲田大学卒業後、ラクスル株式会社、LINEヤフー株式会社にて事業開発やDX推進などに従事した後、株式会社riplaを創業。