近日有三条 AI 新闻，看起来各说各的：Anthropic 宣布 Claude 完成了费马大定理的形式化证明；它同时给自家 API 上了一把锁；国内这边，科大讯飞发布了星火 X2.5。但把这三条摆在一起，会发现它们讲的是同一件事：AI 的价值，正在从「答案」转移到「过程」。谁的过程可验证、谁的过程留得住、谁的过程跑在自己的机器上，成了新的分水岭。一、11 天，1300 万行，一条 358 年的老题先说清楚一件事：Claude 没有重新证明费马大定理。这道题 1637 年由费马写在书页边上，1995 年被英国数学家怀尔斯证出来，原稿 129 页。Anthropic 做的是另一件事——把这份已有证明翻译成计算机能一行一行验证的形式，用的是 Lean 证明助手。别小看这个「翻译」。人类写数学证明会大量省略「显然」「同理可证」这类步骤，而 Lean 不允许——它要你把每一步逻辑都显式写出来。数学家估计，把怀尔斯那份证明完整形式化，可能要花好几年。伦敦帝国理工的 Kevin Buzzard 在 2024 年就发起过一个为期五年的社区项目来干这件事，还发布了 86 页的形式化蓝图。Claude 用了 11 天。生成约 1300 万行 Lean 代码，证明了约 3.03 万个定理，其中约 2.95 万个中间定理最终进入完整证明，整个证明只依赖 Lean 的三条标准公理，规模超过 Lean 核心数学库 Mathlib 的五倍。全程消耗约 60 亿输出词元，用的是一个大致相当于 Claude Fable 5.1 的内部研究模型。真正有意思的是它怎么成的。第一次尝试是失败的。团队最初用标准的多智能体框架，智能体开头进展不错，很快就丢失了整体项目状态，彼此不再有效协作。原因不是模型不够聪明，是架构不对：1300 万行代码、上万个中间定理，没有任何单个智能体的上下文窗口装得下整个项目的状态；多个智能体各干各的，就会重复劳动、互相覆盖，最后谁也不知道还剩什么没做。破局靠一个叫 Prove2Me 的开源平台，由 Anthropic 研究员彭天毅（清华姚班本科、MIT 博士、现哥伦比亚大学助理教授）和哥大的合作者开发。它把所有待证定理组织成一张有向无环图：每个定理是节点，定理之间的依赖是边。新智能体一进来，先查这张图——哪些证完了、哪些正在做、哪些还空着。谁也不重复干活，谁也不会掉队。它还有个工程上的巧思：把定理的陈述和证明拆成不同文件，Lean 只重新编译改动过的文件，于是一个智能体改一处结果，不会触发整份证明重编译。Buzzard 复核了这份成果，评价是：除了数学公理之外没有额外假设，而且证明了「AI 自动形式化的产物已经足够扎实，可以在上面继续盖楼」。为什么这事比「又一个跑分纪录」重要？因为数学界正面临一场验证危机。1998 年黑尔斯证明开普勒猜想，评审团队审了好几年，最后只能给出「高度可信」的结论；2002 年佩雷尔曼的庞加莱猜想证明，数学界同样花了好几年才整理确认。连怀尔斯那份 129 页的证明，发表后都被查出关键漏洞，他和学生泰勒又花了一年才补上。而现在，AI 生成数学成果的速度只会越来越快，人类逐个读完再判断对错，已经不现实了。形式化给出的是另一条路：AI 负责生成，人类负责理解思路，让 Lean 这类系统负责检查逻辑。Anthropic 的展望是，未来的数学论文可能同时提供两个版本——给人读的解释，和给机器验的形式化证明。完整证明已经开源在 GitHub 上。二、几乎同一时间，Anthropic 把「怎么想的」锁了起来9 月 1 日，Anthropic 发布 Claude Fable 5.1，同时在 API 里加了一条不起眼但杀伤力极大的规则，官方归类为「反蒸馏」。要理解它，得先知道什么是「思考块」。Claude 给出最终答案前会先推理，API 会把这段推理过程以思考块的形式返回给调用方；多轮对话时，开发者需要把思考块连同系统提示、工具定义和历史消息一起回传，模型才能接着上一轮继续想。问题就出在这里。有人发现：只要篡改思考块之前的上下文——比如改动早期的系统提示或历史消息——就能诱导 Claude 把原本隐藏的推理过程以明文重新吐出来。蒸馏者拿走的不再只是答案，而是「它是怎么想的」。对推理模型来说，思考过程不是给人看的注释，它就是计算本身。这类模型的做法是把一次性的直觉判断摊开成很多步可检查的推导，用更多词元换更高的准确率。抽走思考过程，模型能力会掉；把思考过程搬走据为己有，等于连人家的计算方法一起搬。差别在哪，可以这么理解：「问题 + 答案」只提供一份监督信号，模型只知道结果对不对；「问题 + 推理轨迹 + 答案」提供的是一整串——哪一步该拆、哪条路走不通、走错了怎么回头。前者教结论，后者教方法。而且更麻烦的是，只抄推理能力的人，往往继承不到配套的安全护栏，造成能力与安全脱钩。Fable 5.1 的做法是加一道服务端硬校验：接口会验证你回传的思考块，是否与当初生成它时的系统提示、工具、历史消息完全一致，不一致直接报错。确有合法修改需求的开发者可以选「非严格模式」——请求照常通过，但受影响的思考块会被删掉，模型在看不见自己上一轮推理的状态下继续作答。生效范围是最容易被忽略的细节：这条规则只适用于 2026 年 8 月 31 日之后创建的新 API 账号，包括 Anthropic 平台新组织，以及 Amazon Bedrock、Google Cloud Vertex AI、微软 Azure Foundry 上的新项目。老账号、Claude Code、网页版和第三方产品里的 Claude 暂不受影响，未来版本会推广到全部用户。有意思的是，这把锁同时还省钱。因为思考块和上下文保持一致，提示缓存命中率大幅提升，Anthropic 给出的预期是典型负载成本比 Fable 5 低约 25%，高智能体化负载最高可降约 45%。封堵和让利来自同一次改动——这说明 Anthropic 不是单纯想赶人走，它更希望开发者老老实实持续调用 API，而不是把能力一次性搬回家。当然，这并没有让蒸馏消失。攻击者仍可以收集普通回答、代码、评分结果和工具调用轨迹，仍可以用代理服务和大量账户分散请求。业内的评价因此分成两派：一边叫好，说常年蹭别人模型的终于被掀了桌子；一边担忧，中小团队原本靠蒸馏追赶，现在这条路窄了，自研和开源路线会更拥挤。还有更直白的说法：表面是反蒸馏，实际是在护定价权。三、国内：讯飞星火 X2.5，全流程跑在全国产算力上第三条是国内的。9 月 7 日，科大讯飞正式发布星火 X2.5 大模型，采用 MoE 架构，参数规模 293B-A30B（总参数 2930 亿、单次激活 300 亿），已在讯飞开放平台上线。这版重点强化的是代码和智能体能力，数学、文本理解等通用能力同步迭代。但真正被关注的是另一句：模型基于全国产算力完成全流程训练及推理，并持续优化国产算力在超长序列训练和推理上的难题。在现在的环境里，这句话的分量不用多解释。前面那条 Anthropic 的新闻说的是「推理过程要锁在自己手里」，这条说的是「训练过程要跑在自己的机器上」——指向的是同一种焦虑。另外，此前开源的星火 X2.5-4B 和 1.7B 两款端侧模型，支持最长 100 万词元上下文，可以本地部署，用在长文档处理、代码辅助、数据分析这类场景上。云上旗舰加端侧小模型，这条产品线算补齐了。过去两年，评价一个模型好不好，看的是它给出的答案。而现在，行业的注意力明显在往前挪：答案是最后一公里，过程才是资产。Claude 那条新闻，是把过程变成可验证的东西——1300 万行 Lean 代码不是给人读的，是给机器一条条查的，查完就知道对不对。Anthropic 改 API 那条，是把过程变成不可搬走的东西——你可以用，但你带不走我的思路。讯飞这条，是把过程变成离不开外部依赖的东西——从训练到推理都在自己的算力上完成。还有个技术细节值得一提：费马大定理那个项目第一次是失败的，救活它的是一张「有向无环图」——一种把项目状态外置、让所有智能体共享的架构。这跟 OpenAI 日前公布的 RSI 数据里那条能对上：智能体数量堆上去没用，长任务零干预成功率仍然卡在 20% 上下，瓶颈不在模型本身，在怎么组织它们干活。对开发者和中小团队来说，能立刻用上的判断有三条：一是别把产品命脉押在单一模型的 API 上，能力随规则变动的风险已经实打实发生了；二是能本地跑的小模型值得重新评估，端侧模型加百万词元上下文，已经能接住不少长文档和代码辅助的活；三是搭多智能体系统时，先设计状态共享机制，别指望堆数量能自动解决问题。
