Astra 把数学证明做便宜了，验收反而更贵

10 项数学与理论计算机科学进展，寻找解法的 token 成本，约 2000 美元。

这三个数字摆在一起，有种很不讲道理的冲击感。

OpenAI 在 8 月 1 日公开了 Astra 的十项研究结果。这些问题横跨高维球堆积、编码理论、非 sofic 群、算术电路复杂度、量子博弈、格密码学和极值组合学。官方给的门槛也不低，每个问题至少十年没有取得主要进展，多数卡得更久。

好家伙，这已经不是模型在竞赛题排行榜上多拿几分了。它开始碰学科里那些长期没有答案的墙，而且一次摆出了十块砖。

可我把 249 页完整论文、62 页发现过程说明 和 Lean 证书仓库 放在一起看，最想聊的反而不是 Astra 到底有多聪明。

我更在意另一件事。

当生成一个候选答案便宜到近乎离谱，验证它、解释它、给它署名并承担责任，会不会变成真正昂贵的部分。

这事跟数学有关，也跟每个正在把 Agent 塞进生产系统的人有关。

2000 美元把答案做便宜了

先把官方那笔账讲清楚。

OpenAI 说，Astra 内部版本找到这十项解法所消耗的 token，按 Sol API 费率估算约 2000 美元。这里说的是寻找这些成功解法的模型 token 成本，不是整个研究项目的总成本。

问题筛选花了多少人力，模型跑过多少没被选中的方向，外部数学家需要多久复核，论文整理和形式化过程用了多少工程资源，官方页面都没有给出完整账单。

所以，拿 2000 美元除以 10，得到一道长期难题只值 200 美元，很爽，也很容易把自己带沟里。

这跟看云厂商账单只盯着一次函数调用差不多。函数跑了 180 毫秒，不代表系统只付了 180 毫秒的钱。日志、存储、重试、人工排障、权限治理和故障值班，全躲在调用之外。

但即使把这层水分扣掉，变化仍然很大。

过去，寻找证明路线通常被一个人的时间锁住。一个研究者一天只能认真追几条思路，走到死胡同还得自己退回来。模型可以同时试很多条路，把失败当成普通的搜索开销。只要单次尝试足够便宜，并行度就会把过去舍不得试的长尾方向全翻出来。

OpenAI 在 5 月公开的 单位距离猜想反例 已经展示过一次这种味道。模型没有顺着主流直觉继续证明那个广受相信的上界，而是尝试构造反例，转而从代数数论里搬来了一套意外的工具。

不是每条野路子都有用。

野路子够多，总有一条会撞开门。

这一下挺要命的。模型最先压低的并不是知识本身的价格，而是「认真追一条可能失败的思路」的价格。研究里的探索预算被重写了，工程里的实验预算也一样。

你做 Agent 时大概见过类似场面。让模型只给一个方案，它会端出一个看起来最稳的平均答案。让它并行生成五个方案，再安排一个独立角色做反例攻击，结果往往更好。以前嫌贵、嫌慢，现在这类搜索正在变成日常配置。

生成端被打穿之后，下一堵墙很快就露出来了。

谁来证明这五个方案不是五种不同的胡说八道。

Lean 不是护身符，是一层验收接口

这次发布最有点子牛逼的地方，是 OpenAI 没只扔出十篇 PDF。

官方同时放出了每项结果的发现过程说明，还把论证形式化成了 公开的 Lean 证书。仓库里能看到 SpherePacking.lean、NonSoficGroup.lean、GapCVP.lean、QuantumParallelRepetition.lean 等独立文件，也准备了逐项检查完整证明的 Comparator 配置。

Lean 是一类形式化证明助手。你可以把它理解成数学世界里极端严格的编译器。自然语言论文可以写「显然可得」，Lean 不吃这套。定义没对上、前提漏了、推理跨了一步，它就不让你过。

空指针。

但这里也得踩一脚刹车。Lean 通过，不等于整项研究自动获得了宇宙认证。

形式化系统检查的是，在给定定义、公理和依赖库的前提下，推导是否成立。它不会自动判断研究问题选得有没有价值，不会替人确认形式化陈述与原始学术问题完全等价，也不会解释一个证明为什么重要。更别提软件工具链本身、依赖版本和形式化边界，同样需要维护。

Lean 更像一层机器可执行的验收接口。

这就很像 CI。测试全绿，只能说明你写下来的断言都通过了。要是测试漏了关键业务路径，绿色对勾照样能把 bug 欢送进生产环境。厉害了，所有检查都成功，用户的钱没了。

真正靠谱的流程，不会把绿色对勾当护身符。它会把验收拆开。

自然语言手稿负责让同行理解论证，Lean 负责把推理链压到机器可检查的粒度，发现过程说明负责暴露模型怎么走到这里，数学共同体再判断结果的意义、上下文和边界。

四层东西各自做一件事，互相不能冒充。

这比「模型生成，另一个模型打分」扎实多了。后者常见的问题是，生成者和裁判共享同一套盲区，甚至共享同一种讨好人的语气。两个模型互相点头，不叫共识，只能叫回声。

OpenAI 也没有假装争议已经结束。官方页面专门回应了数学共同体对 AI 参与研究的担忧，并链接了 Leiden AI 与数学宣言。那份宣言关心的不只是证明对不对，还包括透明度、署名、教育、权力集中和研究文化。

答案有了，问题并没有少。

只是问题从「能不能得到结果」，往「谁能检查结果、谁能理解结果、谁有资格决定结果算什么」挪了一大截。

把这套流水线抄回 Agent 工程

数学离普通开发者很远，Astra 这套分层却不远。

很多 Agent 项目仍然把一次漂亮输出当成完成。模型写了一段迁移脚本，看起来没毛病。模型改了一份合同，语气很专业。模型总结了一轮用户访谈，表格也齐。

然后就准备 merge。

段错误。

如果把 Astra 的工作流翻译成工程语言，大概会得到一条很朴素的链路。

任务定义要先冻结，候选方案允许并行探索，成功候选要转成可执行断言，机器检查只能覆盖明确写出的边界，还得由拥有领域责任的人做语义验收。

注意，这不是让每个团队都去学 Lean。别给 CRUD 再造一门形式化语言，项目经理会追着你跑。

你需要的是为自己的任务找到那个「可以编译的真相」。

写代码时，它可以是单元测试、类型检查、静态分析、集成测试和可重复 benchmark。让 Agent 改数据库迁移时，它还得包括回滚演练、行数对账、约束校验和影子流量。

做数据分析时，它可以是固定查询、口径检查、抽样复算和来源链接。图表看起来再顺眼，只要分母偷偷换过一次，结论就该回炉。

处理文档时，它可以是 schema、必填字段、引用可达性和版本差异。总结类任务最容易被流畅语言骗过，能把每个关键判断指回原文位置，比再加一句「请仔细检查」有用得多。

涉及真实动作时，验收还要加一道权限闸门。模型可以草拟邮件，不能因为置信度写了 0.97 就自行发给客户。模型可以准备付款单，不能把金额格式正确当成付款理由成立。

坦率讲，这些东西一点都不性感。

它们像 CI 里那些让人嫌慢的检查，像数据库迁移前那份没人想看的回滚方案，像告警规则里一个又一个乏味的阈值。演示视频不会给它们镜头，事故复盘里倒是每页都有它们。

模型越能干，验收层越不能只靠感觉。

因为输出规模上去以后，人类不可能逐字重做一遍。要是每个结果都必须让专家从头推到尾，自动化只是在上游制造了更多待审批工单。省下来的生成时间，会原封不动地堵在复核队列里。

所以验收也得工程化。把能自动判断的部分写成检查，把不能自动判断的部分压缩成人类真正需要看的差异，把风险高的动作留在明确的确认点，把失败结果送回局部重试，而不是整条链路从头再来。

这才是我觉得 Astra 最值得抄的地方。

不是那十个答案。

是答案后面那套可检查、可追溯、能返工的结构。

最贵的那张账单叫责任

官方在署名问题上说得很直接。数学论证由系统生成，人类协助准备手稿和形式化，并对正确性负责。把一份完全由 AI 生成的证明写成人类独立成果，会同时歪曲系统贡献和人的智力劳动。

这段话比 2000 美元更值得反复看。

如今很多团队还在用一种含糊写法，AI 参与了一切，但成果页上只留人名。另一些团队走向另一个极端，把锅全推给模型，仿佛「AI 生成」四个字是一张免责贴纸。

两边都省事，也都不诚实。

署名是贡献记录，责任是风险归属，验证是证据链。这三件事有关联，却不能糊成一个字段。模型生成了候选方案，不代表模型能承担后果。人类点了确认，也不代表全部智力工作都由人完成。

对普通团队来说，最实用的做法可能很土。

给每次高风险输出留下来源、模型版本、提示输入、工具调用、机器检查结果和人工确认人。别只存交付时那段漂亮文字。出了问题之后，大家真正需要的是知道哪一步开始偏、哪一道闸门没拦住、应该只重跑哪一段。

这跟数学证明的公开包其实是一回事。论文是交付物，Lean 文件是机器证据，发现过程是搜索轨迹，责任声明是边界说明。

生成成本会继续往下掉。今天是十项数学进展约 2000 美元，明天可能是几百美元，后天甚至只是某个订阅套餐里没被单独标出来的一小截额度。

可验证不会免费，理解不会免费，承担责任更不会免费。

我可能看得太工程师了，但这大概就是接下来几年最真实的成本迁移。过去我们付钱买答案，后来付钱买速度，再往后，真正稀缺的会是让答案值得相信的那套制度和工具。

模型负责把海面上的航线画得越来越多。

人要做的，是把灯塔、浮标和暗礁标清楚。

否则 2000 美元买来的不一定是十条新航路，也可能是十艘同时开得很快的船。