#Lean-4

OpenAI、次期モデル「Astra」を発表 未解決数学問題10問を機械検証済みで解決

OpenAIは2026年8月2日(現地時間)、次期主要モデルとなる「Astra」が、少なくとも10年間未解決であった数学および理論計算機科学の10問に対し、新たな結果を生成し、機械検証可能な証明を公開したと発表した。同社は249ページに及ぶ原稿集、モデルによる推論ウォークスルー、およびLean 4による証明書を公開している。証明書はGitHub上でApache 2.0ライセンスの下で利用可能となっている。