OpenAIは2026年8月1日、未公開の新モデル「Astra」が数学・理論計算機科学分野で10個の長年未解決だった問題を解決したと発表した。証明はすべて形式証明言語Lean 4による機械検証可能な証明書として公開され、専門家でなくても第三者が結果を独立に確認できる点が注目を集めている。
群論からエルデシュ問題まで、多分野にわたる10件の成果
Astraが取り組んだ問題は複数分野にまたがる。群論では、数学者ミハイル・グロモフが1999年に「ソフィック群」の概念を提示した。以来27年間未解決だった非ソフィック群の構成問題を、Astraが解決した。作用素環論では、フィールズ賞受賞者アラン・コンヌが1980年に提唱した「コンヌ剛性予想」を反証した。
エルデシュ問題（未解決の数学問題集）では、多色ラムゼー数に関する183番を含む3件を解決した。このほか、1978年以来更新がなかった高次元での球充填密度の改善にも成功した。さらに量子ゲームにおける並列繰返定理やパーマネント計算の回路計算量下界も解決した。格子暗号を用いた耐量子暗号分野でも進展があり、幅広い成果を挙げた。
Lean 4による機械検証という新基軸
すべての証明にはLean 4の証明書が付属し、GitHub上でApache 2.0ライセンスの公開リポジトリとして公開された。Lean 4の「信頼されたカーネル」は、証明がコンパイルされるか否かで合否を判定する二値的な検証方式である。専門家の主観的評価に頼る従来の査読とは、この点で異なる。OpenAIによれば、10問すべてを解くのに要した計算コストは、Sol APIの料金換算で約2,000ドルだったという。
専門家の評価と、過去の教訓
エルデシュ問題を集約するサイト運営者でもあるマンチェスター大学の数学者トーマス・ブルーム氏は、今回の成果を「大きなニュース」と評価した。Astraが2026年5月に手掛けた単位距離予想関連の成果より重要だとも述べている。一方、OpenAIのノーム・ブラウン氏は「残念ながらミレニアム懸賞問題はまだ解けていない」と述べ、過大評価を戒めた。
今回の発表の背景には、2025年10月の経緯がある。当時OpenAIはGPT-5がエルデシュ問題10件を解決したと発表した。しかし実際は既存文献の解法をそのまま示していただけだとブルーム氏に指摘され、OpenAIは発表を撤回した。今回は機械検証と第三者による独立評価が伴う点で、構造的に異なるとされる。
Astraは現時点で一般公開されておらず、大統領令14409に基づく米政府の事前審査を経る見通しだという。数十年来の難問に機械検証可能な証明で挑んだ今回の成果は、AIによる数学研究の信頼性を高める一歩として今後も注視される。
参考：OpenAI's Astra Solves Ten Decade-Old Math Problems With Machine-Checkable Lean Proofs