OpenAIは、同社が研究開発を進める数学・理論情報学特化型AIモデル「Astra」が、理論数学分野において数十年間未解決であった難解な問題10件の解法を自律的に発見し、形式的検証を完遂したと発表しました。
本研究では、コンピュータによる定理証明言語「Lean」を用いてAIが導出した解法プロセスの正当性を数学的に完全検証しています。
単なるテキスト生成にとどまらず、論理的な矛盾を含まない完璧な数理的証明を自律構築できる能力を示しました。今後の暗号プロトコルの安全性検証、高度なソフトウェアアルゴリズムの最適化、ならびに先進科学分野での基礎研究におけるAI活用を劇的に飛躍させる歴史的成果として評価されています（一次ソース：OpenAI公式発表）。