OpenAIは数学と理論計算機科学の未解決問題10件に関する研究成果を公表した。
解決または大幅な進展を示した各結果は、次期主要モデル「Astra」の内部版が生成したという。
次期モデルAstraが未解決問題10件に挑戦
2026年8月1日にOpenAIが公開した成果は、高次元球充填、符号理論、群論、算術回路計算量、量子計算量、格子暗号、極値組合せ論など幅広い分野に及んだ。
示された10件の成果のうち、非ソフィック群の存在証明やConnesの剛性予想への反例、Erdős問題183などでは長年の問いを解決したとし、ほかの課題でも新たな上界・下界や近似困難性を示した。
これらの数学的議論は、同社が開発中の次世代モデル「Astra」の内部バージョンが生成したという。解答探索に必要だった総トークン量は、同社のSol API料金に換算して約2,000ドル相当とされる。
その後、人間が同じモデルを用いて論文原稿を整え、モデルが各議論をLean証明書（※）として形式化した。
OpenAIは5月にも、未公開モデルの評価中に得られたErdősの単位距離予想への反証を発表していた。今回の公表は単発の成果ではなく、研究開発段階のモデルを実際の未解決問題で継続評価していることを示すものだ。
なお同社は、AIが全面的に生成した証明を人間の著作として示すのは不正確だとの立場を表明している。
※Lean証明書：定理証明支援系Leanで、証明の各推論が論理規則に従うかを機械的に検証できる形式データ。人間による査読を代替するものではないが、形式上の誤りを発見しやすくする。
研究加速への期待と検証・帰属の課題
Astraの成果が専門家による検証を経て定着すれば、AIは既知の知識を説明する道具から、新しい定理や反例の候補を生み出す研究協力者へ近づくだろう。
特に、複数分野にまたがる探索を比較的低い計算費用で進められる点は、大学や企業の研究速度を押し上げる可能性がある。
一方、OpenAIの研究だけで10件すべての正しさや学術的価値が確定したわけではないと考えられる。形式検証は論理的一貫性の確認に有効だが、前提設定の妥当性、既存研究との重複、成果の重要性は数学者による精査が不可欠になる。
また、モデルが生成した証明を誰の業績として扱うかという帰属問題も避けられないはずだ。
今後はAstraの公開形態や再現性に加え、第三者が結果を検証し、引用や著者表示の規範を整えられるかどうかが焦点となりそうだ。
関連記事:
Google DeepMindの数学AI、56年未解決問題を含む9件を形式証明 研究レベルの数学にAI活用広がる
高校数学がAI時代向けに再編へ 行列・確率・統計を横断的に学ぶ新体系
