据动察 Beating 监测，OpenAI 首次正式公布下一款主力模型 Astra。内部版本在 10 个长期未解的数学和理论计算机科学问题上取得新结果。这些问题的核心结论至少 10 年没有进展，多数停滞时间更长。 其中一些问题被直接解决或推翻。Astra 首次构造出非 sofic 群，回答了群论中的一个核心开放问题；它还推翻 Connes 刚性猜想，并解决 3 个 Erdős 问题。其余成果包括球体堆积、编码理论、量子复杂性和后量子密码相关问题的新上下界与困难性证明。 OpenAI 称，模型找到这 10 项结果所用的 Token，按 Sol API 价格折算约为 2000 美元。 这些数学论证由 Astra 生成。人类随后协助整理成论文，模型再把每项证明转成 Lean 证书，让计算机逐步核验推导是否成立。OpenAI 已公开论文、证明证书和模型的推理过程。