OpenAIは次期主力モデル「Astra」により、少なくとも10年間進展のなかった数学・理論計算機科学の10件の課題（球充填密度の改善、並列反復定理の拡張、ラムゼー数の下限証明など）で新たな成果を報告しました。解の探索に要したトークン費用は約2,000ドル相当で、249ページの論文と検証可能なデータがGitHubで公開されています。
注目すべきは「AIが解いた」こと以上に、生成した証明を Lean 4 で形式化し、機械検証可能にした点です。LLMの出力には常にハルシネーションの懸念がつきまといますが、形式検証を通せば正しさの担保を人手に頼らずに行えます。AIによる知識生成の信頼性を保証する枠組みとして重要な一歩と言えます。