「AIがコードを生成できるなら、数学の証明も生成できる」は直感的に正しそうだが、「その証明が正しいと確認する」のが誰の仕事になるかは、まだ決まっていない。
「解いた」をめぐる議論の構造
OpenAIのエージェントが数学の未解決問題「ミレニアム懸賞問題」の一つを解いたと発表した（2026年9月）。しかし発表直後から数学コミュニティで論争になっている。論点は「証明の形式」ではなく「証明の検証可能性」だ。AIが出力した証明は機械的な検証ツール（Lean、Coqなど）で自動確認できておらず、「解いた」の定義が生成と検証で分裂している。
flowchart LR
A[問題の定式化] --> B[AIによる証明探索]
B --> C[証明の出力]
C --> D{形式検証ツール}
D -->|成功| E[自動承認]
D -->|失敗・未対応| F[人間による検証]
F --> G{承認?}
G -->|Yes| H[証明として承認]
G -->|No| B
style A fill:#7f8c8d,color:#fff
style B fill:#2980b9,color:#fff
style C fill:#2980b9,color:#fff
style D fill:#7f8c8d,color:#fff
style E fill:#2980b9,color:#fff
style F fill:#e67e22,color:#fff
style G fill:#e67e22,color:#fff
style H fill:#2980b9,color:#fff
で、実際のところは
形式的証明ツール（Lean 4など）を使ったワークフローでは、AIが証明のステップを提案し、人間がそれをチェックする「Human-in-the-loop」が前提だ。今回のケースはその前提を超えている——AIが独立して証明全体を生成し、人間による確認が追いついていない。エンジニア的な影響として、証明探索は計算コストが跳ね上がる（o3クラスの推論モデルを前提とした見積もりが必要）。またプロンプト設計の観点では、「証明を生成して」より「このステップの反例を探して」という問い方のほうが、実用的なフィードバックを得やすい。
検証なき「解決」というトレードオフ
ベンチマーク上の数学スコアが高いことと、コミュニティが承認できる形で証明を提示することは別の話だ。現状のAIは「見かけ上整合した長い証明」を生成できるが、そこに論理的な飛躍が混入していても人間が追跡しにくい。証明の長さが増すほど誤りの隠れ場所も増える——形式検証ツールへの自動変換ができない証明は独立した数学者の目が必要になり、スケールしない。「コンテキスト長が増えれば深く考えられる」とは限らない、を地で行く事例でもある。
一つ問いかけ
あなたが書くコードの中で「正しさを証明できれば最も価値が高い」部分はどこか——そこに形式検証を導入するとしたら、AIはどのステップを担えるか？
参考: What OpenAI’s latest controversy tells us about the future of math – MIT Technology Review