Astra：AI在原创数学发现上的一次实质性突破2026年8月1日，OpenAI在一篇看似低调的博客里写下了这样一句话：“The results were achieved by an internal version of Astra, our next major model.”这句话的分量，远比大多数人第一眼看到的要重。因为紧接着，他们公布了十个结果。不是刷榜、不是在已知问题上提高几个百分点，而是十个至少开放了十年以上的数学与理论计算机科学问题，被一个尚未公开发布的模型解决了。每一个结果都附带了完整的Lean 4形式化证明，机器可以直接验证，没有sorry，没有人工补洞。这不是“AI辅助发现”，而是AI主导完成了可验证的原创性数学工作。这些结果为什么重要？先说最显眼的几个：- 非sofic群的首次显式构造。自1999年Gromov提出soficity概念以来，数学家们一直在问：是否存在无法被有限置换系统任意逼近的群？这个问题悬空了27年。Astra给出了第一个明确的例子。- Connes刚性猜想的反证。这个猜想涉及冯·诺依曼代数与群结构之间深刻的对应关系，长期被认为可能成立。Astra构造出了反例。- Ehrhart体积猜想的证明，以及三个Erdős问题的解决（其中包括多色Ramsey数相关的难题）。- 高维球堆积密度上界自1978年以来的首次实质性改进，达到了Cohn–Elkies阈值。这些不是边角料。它们横跨群论、算子代数、高维几何、编码理论、量子复杂度、格密码学和极值组合学。更关键的是，OpenAI表示，找到这十个解所消耗的token成本，按当前Sol API价格计算，大约只有2000美元。效率高到几乎让人感到不真实。真正让人警惕的，是方法本身Astra被描述为面向长周期任务的模型。它不是单次对话、单次推理，而是一个能把复杂问题拆解、分配给多个子Agent、等待结果、再综合的系统。根Agent可以持续工作数小时甚至更久，而不是在几十秒内给出一个“看起来合理”的答案。这意味着两件事：1. 它开始具备持续探索未知的能力，而不是在训练数据的影子里打转。2. 它输出的不是自然语言叙述，而是可以被机器严格验证的形式化证明。幻觉的空间被大幅压缩。过去几年，我们看过太多“AI解决了某某数学问题”的新闻，事后往往发现是提示工程、人类大量干预，或者结果经不起严格审查。这一次不同——证明被公开在GitHub上，任何人都可以用Lean重新检查。这是质变的信号。为什么这让人觉得Astra可能会脱颖而出？当前主流大模型（包括GPT-5.6系列）已经在编码、工具使用、多模态理解上达到了很高水平。但它们大多仍在“重组已知知识”的范畴内运作。真正的科学发现需要另一层能力：在没有现成路径的地方，提出新结构、新视角、新证明策略。数学是这种能力最严苛的试金石。它几乎完全依赖抽象与逻辑，几乎没有“从例子中统计规律”的捷径。当一个模型能在这种环境里持续产出可验证的新结果时，它已经不再只是“更强的语言模型”，而开始接近某种能够参与知识创造的系统。Astra目前展示的，正是这种能力的早期形态。它还没有公开发布，正式版本可能还会经过美国联邦安全审查。我们不知道它最终会以什么名字出现，也不知道它在更广泛任务上的表现如何。但已经公开的证据足够说明一件事：OpenAI在内部，已经把“让AI真正参与原创科学发现”这件事，推进到了一个相当具体的阶段。如果后续更多领域（物理、材料、生物、甚至开放式工程问题）也能看到类似质量的结果，那么Astra很可能成为我们第一次认真讨论“接近AGI”时，必须正视的那个模型。不是因为它会聊天更自然，也不是因为它写代码更快，而是因为它开始做一件过去只有人类顶尖研究者才能做的事，在未知的边界上，留下自己的脚印。