1. OpenAIが実際に公開したもの

OpenAIは2026年8月1日、高次元幾何、符号理論、群論、回路計算量、量子計算量、格子暗号、凸幾何、ラムゼー理論にまたがる10件を発表した。数学的議論は次期主力モデルとする社内版Astraが生成し、人間と同モデルが原稿とLean証明を整えたという。

現行原稿は253ページで「2026年8月6日更新」と原版へのリンクがある。これは改訂可能な研究公開であり、Astraの一般提供や最終的な学術誌記録ではない。8月17日時点でOpenAIページはこの集合を受理した査読誌を示していない。

2. 10件すべてが同じ意味の完全解決ではない

OpenAI自身が「解決または大きな進展」と表現する。非ソフィック群の構成やConnes剛性予想の反例がある一方、球充填と符号の境界改善も含む。論文は球充填の一般指数について1978年以来初の改善とするが、境界改善は全場合の分類とは違う。

正確な見出しは性質の異なる10件の形式化貢献であり、「Astraが未解決問題を10問解いた」ではない。範囲、先取性、重要性は各分野の専門家が文献内で判断する。

  • 解決・構成：存在を証明し、提示された問いを閉じる。
  • 反証：予想への反例を与える。
  • 境界改善：既知値を進めるが全側面を終えない。
  • 形式証明：論理を検査するが重要度は評価しない。

3. Leanが保証する範囲

All.leanは成果ごとの10モジュールをimportし、リポジトリはLean 4.32.0、mathlib、Lakeを指定する。Lean公式マニュアルによれば、カーネル受理はファイルと依存先の定義・定理・公理から形式命題の証明が従うことを意味し、適切な検証は未完了目標やタクティクの誤りを検出する。

OpenAIは隔離環境と外部チェッカーを使うComparator課題も公開した。信頼する命題を固定し、単一ビルド経路への依存を減らす強化策だ。それでも形式命題が共同体の意図した予想と同一かという意味上の問いは人が確認する。

4. 証明書が埋めない四つの空白

第一は翻訳で、正しいコードが見出しより弱い命題を表す可能性がある。第二は新規性で、カーネルは文献検索も再発見検出もしない。第三は重要性で、論理的妥当性は深さや有用性を保証しない。第四は帰属で、証明書は参考文献の完全性や訓練資料の権利を証明しない。

ライデン宣言は開示、人間による説明、適切な形式検証を推奨しつつ、人間の責任と査読出版の継続を求める。Leanへの反対ではなく、科学的信頼の連鎖の中に位置づける考え方だ。

  • Lean：符号化した導出は受理されたか。
  • 分野査読者：翻訳・先行研究・新規性は妥当か。
  • 学術誌：方法・帰属・重要性が独立審査を通ったか。
  • 機関：特権的モデルアクセスなしで再現できるか。

5. 2,000ドルという数字の意味

OpenAIは解を「見つけるために必要だった」総トークンをSol API価格で換算すると約2,000ドルとした。これはトークン価格の換算で、プロジェクト会計ではない。失敗試行、問題選択、Astraの訓練計算、人間の時間、253ページの原稿、形式化と審査費が含まれるか明確でない。

従って数学問題10件が総額2,000ドルで解けたとは言えない。成功発見の限界推論費が研究者時間に比べ極めて低くなる可能性は大きいが、アクセス条件、命中率、人間検証費が自動数学研究所の経済性を決める。

6. 日本の大学・研究機関の調達基準

導入評価では非公開の評価問題、再ビルド可能な証明、分野専門家2名の審査、失敗実行・トークン・人間時間の台帳を求める。発見費と、理解可能で出版可能な証明へ変換する費用を分けるべきだ。

初期用途は仮説探索、補題提案、既知段階のLean形式化とし、先取権を発表する前に実名の人間承認者を置く。日本の強い定理証明・ソフトウェア検証文化を、モデル評価だけでなく公開可能な検証基盤へつなげる好機でもある。

  • 固定版のツールと依存関係で再ビルドする。
  • 形式命題と自然言語主張を行ごとに照合する。
  • 広報前に独立した先行性調査を行う。
  • 成功トークンだけでなく失敗と審査費を公開する。
  • 正確性・引用・影響の人間責任者を明記する。