OpenAI、数学・計算機科学の難問 10 件を解いた未公開モデル Astra を発表──全証明を Lean 4 で検証
長年未解決だった 10 件の数学の難問を未発表モデル Astra が解き、Lean 4 の機械検証済み証明を GitHub に公開した。
リリース: 2026-08-03 · 読了 3 分記事の要約
1. 核心（What）
- OpenAI が未発表モデル Astra を用いて、数学・計算機科学の 10 件の未解決問題を解決し、249 ページの論文と Lean 4 の証明コードを公開した。
- 1999 年からの非ソフィック群の構成や 1980 年提唱の Connes の剛性予想の反証など、8 分野にわたる新しい数学的成果を達成した。
- 全 10 件の証明は Lean 4 により機械検証されており、GitHub に Apache 2.0 ライセンスで公開されている。
- 全解の導出にかかった総推論コストは GPT-5.6 Sol API レートでおよそ 2,000 ドルと報告されている。
2. 影響（Why）
- 形式検証を伴う数理推論の確立: ハルシネーションの混入しやすい自然言語の数学表現を排し、Lean 4 による完全な機械検証を通過した証明を生成したことで、実科学への LLM 実装の信頼性が一線を越えた。
- 国内研究組織への検証負荷: 国内の数理・暗号系の研究組織は、AI が生成した膨大な定理証明の妥当性を検証するための Lean 4 エンジニアリング体制の確保を迫られる。
3. 根拠・詳細（How）
- 長期マルチエージェント推論設計: 長時間の複雑な探索タスクを実行する長期マルチエージェント推論アーキテクチャを採用し、高次元球充填や量子並列増幅などの難問に対して段階的な証明探索を実行。
- Lean 4 による完全機械検証: 出力されたすべての証明は定理証明系 Lean 4 のチェッカーを通過しており、未証明のギャップを含まない厳密な証拠として 249 ページの原稿と共に公開された。
4. 展望・課題（Next）
- Astra の一般公開時期は未定: モデルの一般公開日や価格体系、API の提供時期については現時点でアナウンスされていない。
- 学術界の帰属ポリシーへの影響: OpenAI が AI による著作者表示を明言したため、学術雑誌や大学における研究論文のクレジット表記の見直しが進む見通し。