8 月 1 日一晚上，10 道数学题被一个未发布的内部模型拿下。Lean 4.32.0 编译，sorry 计数 0，249 页手稿，62 页 walkthrough，Apache-2.0 公开仓库，token 成本约 2000 美元。8 月 7 日同一周，同一模型被 OpenAI 自己暂停部分研发，模型权重加密，等待美国政府 CFT 框架审查。
一周之内，同一个模型，先破数学后被锁。这两件事其实是一件事。
先把数字摆清。10 道题覆盖 8 个子领域——群论里给出非 sofic 群的显式构造（Gromov 1999 年提出，悬了 27 年）；von Neumann 代数方向证伪 Connes 刚性猜想；高维几何方向给出球体堆积密度上界（1978 年以来首次推进）；Erdős 三题（146/180/183）；permanent 公式下界 n^4/log n；量子游戏指数并行重复；CVP 多项式因子硬度。
但 Gary Marcus 在 X 上用了一个词：「amazing but vastly oversold」。我同意。
第一，5 道题是真正的「猜想解决」——非 sofic 群、Connes 反例、Ehrhart 体积、183 多色 Ramsey、Erdős 146/180。剩下 5 道是改进已知界——比如球体堆积是把上限压到 Cohn-Elkies LP 阈值，但没给出新构造。这意味着「Astra 解了 10 道开放数学」是个粗略叙事，真实情况是「10 道里有 5 道是真突破，5 道是高质量边界推进」。这个区分对真正在跟这套文献的人很重要。
第二，2,000 美元是 token 推理成本。不含人工撰写手稿、不含模型训练、不含 Beta 测试。OpenAI 研究员参与了论文撰写与形式化——这条不能藏在营销话术里。Noam Brown 公开确认：没有 Millennium Prize 问题被解出来。
第三也是最关键的一条：Astra 当周被锁了。OpenAI 历史上第一次认定自家某款模型「可能触及关键级网络安全能力门槛」。措施包括暂停部分研发、隔离测试环境、限制网络与工具访问、权重加密、实时监控。这意味着前沿模型单点能力突破的速度，正在逼近监管能跟得上的上限——同一周等于用一次自家产品自证：前沿模型研发的下一个真正限制，不是算法也不是算力，而是「能否在不同时期分别放出不同片段」的安全门设计——这本身才是真正的研究问题。
下一根钉子：当 Polymarket 上 Astra 8 月 31 日前发布概率从 24% 升到 50%+，意味着模型安全审查正在快速通过；反之如果延期到 Q4，说明 CFT 框架已经把「关键级」定义卡在了更严的位置。无论哪种情况，Lean 4 证书公开这件动作都比 Astra 何时发布更重要——它给整套 AI 科研划了一条新基线：「可机器核验」是新的发布标准，不是 peer review 的替代品。
#OpenAIAstra #Lean4 #CFT审查