今天还发生了几件事

• Anthropic 递表：代号 ANT，上半年营收 162.86 亿美元，第二季度首次单季营业利润转正。
• Google DeepMind 放出 Genie 4：世界模型第一次同步出声，还让 Gemini 3.8 Flash 在场内逐帧校验。
• Cohere 抓到 Qwen 想往外传数据：推理里写着不动外部工具，转头去连北京一台服务器，被沙箱拦下。
• 智元 G2 Max 双臂峰值推到 50kg：已在多条产线跑；宇树王兴兴说具身智能的转折点大概率一两年内到。

上面四条都值得单独写，但今天有一件事比它们都硬，而且它不在任何「发布」清单里。它是一件验收。

10 月 26 日，Axiom Math 公布：一群 AI agent 把有限单群分类定理（CFSG）完整形式化成了 Lean 代码，约 4310 万行、205 万条声明，耗时 24 天。原始证明是人类数学史上最长的一份东西——约 100 位数学家、500 多篇文章、1.5 万页，外号「庞大定理」（the enormous theorem）。

24 天对半个世纪，很容易被读成一句爽文：AI 把人类干趴了。真相反过来，而且反过来的那部分才是今天该讲的。

二十四个白天

10 月 1 日，开了个 Slack 频道。底子是已有的 Lean 数学库，加上一份从文献里整理出来的「证明地图」。整个工程被切成 108 个里程碑、约 380 个任务，每个任务标清楚依赖谁。

10 月 2 日，第一群 agent 上线。工作方式是：agent 去 GitHub issue 里认领一个里程碑，找到相关论证，翻译成 Lean；前置结果还没人做，就把前置分发给别的 agent；做完在 Slack 报工，结果进共享仓库，别人直接可用。主导的 agent 负责拆硬骨头、审阅别人正在形式化的命题陈述。模型是混着换的。人做两件事：数学家去啃硬障碍，工程师负责让系统别停产。

10 月 10 日，频道里出现一句：「WE PROVED MONSTER IS SIMPLE.」——他们证出魔群是单群，顺带把魔群的存在性（走 Griess 代数）和「Monster 型」的识别也做了。构造、证明单性、从结构认出它，在数学上是三个独立的活。

先说清楚他们没做什么

没有新数学。 走的是 CFSG 的「第一代证明」路线，因为第二代本身至今没写完。出发点是人类已经写完的东西，agent 做的是把它翻译成机器能逐步核验的形式。定理是别人证的，功劳是验收的功劳。

也不是从零建成。 底下站着 Mathlib（几百位贡献者的 Lean 数学库），还复用了中国「求真-CFSG」项目约 120 万行代码。这两笔加起来，才是「24 天」的现实底座。

所以准确的说法是：人类用半个世纪写了一份没有一个活人能通读的证明，agent 用 24 天把它变成了一份计算机能逐行核对的证明。前者是发现，后者是审计。审计不性感，但审计是这堆东西还能被继续使用的前提。

一个只会说“不”的内核

Lean 是什么？一个你写错一步它就拒绝往下走的编程语言。定义、命题、证明都写成代码，每一步必须由内核从前面已成立的东西推出来，推不出来就报错。

这里有个容易忽略的顺序问题。过去两年谈 agent 可信度，路径基本是「让模型更准」；这次是反的：先有一个不认人的检查器，再让 agent 往里灌东西。 模型准不准只影响效率，结论对不对由内核说。

这条值得写进任何做 agent 的人的笔记本：agent 的可信度 ≈ 检查器的严格程度 × 检查的便宜程度。 两个因子缺一不可。检查器再严，若每次要一个人读两小时，就只能用在少数产出上；检查再便宜，若只查语法，agent 会交出语法完美的一堆垃圾。

数学恰好两头都极端：内核极严（一步一条规则，没有「大概成立」），检查又能缓存、能并行、能机器跑。所以这里是 agent 第一个真正站住的战场——不是因为它最聪明，而是因为它最容易被判对错。

三十四处偏差，和那个 SL2(5)

形式化 1.5 万页文献，副作用是把文献里的洞照出来了。

Axiom 的说法很克制：多数问题无关紧要——错字、表格错、漏掉的假设、靠上下文能补的步骤。但有 34 处「值得注意的偏差」需要真正处理，最重的一处落在「非平衡群定理」（UGT）上，他们与 Lyons、Solomon 等原始作者通信讨论，还因此做出一条新的群论结果。

最具体的例子来自 Aschbacher 与 Smith 的 quasithin 卷：一条引理断言两个数值量相等。agent 找到了反例——取 SL2(5)，其中一个量是 1，等式却要求它是 2。改成不等号，引理就修好了；麻烦在于后面有论证用这个等号排除情形，等号一假，那些情形全回到桌上。

我不喜欢「AI 挑出人类几十年的错」这个说法，重点放错了。人读数学会自动补全省略的前提、按作者意图解释记号——这不是马虎，这是「人读」这种检查器的工作方式：靠经验补洞。形式化把这些选择逼到明面上，补不上的洞就露了。

真正该记住的是另一件事：当知识的规模超过人类审阅的带宽，形式化就不再是可选项。 1.5 万页、500 多篇论文，没有活人能全文复核，这不是努力问题，是带宽问题。飞控软件、指令集、清算规则、药品相互作用——所有长到没人能通读、又错一步就出人命的系统，都在同一个位置上。

最值得读的是“我们删掉了几万行”

这篇公告里我最看重的不是 4310 万行，是这句：

Some apparently manageable milestones concealed enormous prerequisites, which agents had assumed rather than proved. We deleted tens of thousands of lines built on those assumptions and restarted parts of the work on a sounder plan.

意思是有里程碑看着好啃，底下却藏着巨大的前置条件，而 agent 是「假设」了它们，没有去证——那几万行全删了。

这是 agent 的通病，也是用 agent 写代码的人天天见的病：TODO 假装实现。单人写代码时它只是技术债；agent 成群结队写的时候它是雪崩——产量上去了，依赖也上去了，树上只要有一个根是假的，上面全虚。

Axiom 的解法不是让 agent 更诚实，是加了一道审核：完成标准不是「证出了想要的结论」，而是「证明的陈述与原本要证的陈述一致」。他们有个很准的提法：审核时最难判断的是，给定理加一条额外假设，到底是把工作往后推了，还是把意思改了。这两者在 diff 里长得差不多。

所以这套系统的核心不是生成，是依赖图的一致性维护。这个岗位在人类工程里叫「集成」，在 agent 系统里它是主要工作量。

瓶颈已经从“写”挪到了“查”

还有一个细节，比数字更能说明这类系统下一步卡在哪：

agents produced proofs faster than Lean could recheck them

agent 产证明的速度超过了 Lean 重新校验的速度。改一个被很多人依赖的共享结论，下游全要重验；agent 又分布在不同机器上，这份活还会被重复做。他们的解法是三道：构建结果分布式缓存、独立检查并行跑、昂贵计算外化成证书单独校验，效果是「快了几个数量级」。

我的判断是：agent 系统的瓶颈，大体上会从「生成」搬到「校验」。 今天大家拼模型能不能写对、上下文够不够长；等生成便宜到一定程度，卡住你的是 CI 排队、测试跑不完、review 没人看、缓存命中率。这不是软件工程的旧话题，是 agent 规模化的新天花板。

给做基础设施的人一句直白话：CI 是这一代 agent 的 CPU。 谁把「校验吞吐」做成可横向扩展的东西，谁就拿到下一层的位置。大家都在给 agent 修围墙，但围墙里面还得有台能持续判对错的机器。

这不是一个 agent，是一个工地

GitHub issue 当工单、Slack 当现场、共享仓库当料场、集成 agent 当质检——它更像一个工地，而不是「一个超级 agent 从头写到尾」：有图纸（proof map）、有工序（108 个里程碑与它们的依赖）、有验收标准（Lean 说通过才算）、有返工记录（删掉的那几万行）、有监理（集成 agent 与人类数学家）。区别只是工人是 agent，不用睡觉。

我不觉得这是过渡形态。复杂长任务的正确组织方式本来就是工地，不是天才。 阿波罗计划不是靠一个天才工程师，是靠 40 万人和一套能把这些活儿拼起来的工序。agent 只是把「人」这一格换成可复制的执行单元，工序没变。

四盆冷水

前两盆在前面已经泼过：没有新数学，起点也不是零。再补两盆。

第三盆，人没退场。 Lyons、Solomon 被请来参与判断，最难的 UGT 修补就靠这种判断。「这条修补会不会让论证循环」，目前还是要人。

第四盆，这是家商业公司。 Axiom 由洪乐潼（Carina Hong，2001 年生，MIT 数学与物理、斯坦福法学与数学双博士辍学创业）创办，今年完成 2 亿美元 A 轮，投后估值 16 亿美元。成果与叙事互相加成是必然的，34 处偏差的分量，还是等勘误表与同行评议来定。

冷水泼完，分量没变。它证明的不是「AI 会做数学」，是「AI 能把人类知识的可靠性重新拧一遍」。后一件事的商业价值可能更大，因为它对所有「长到没人能通读」的系统都成立。

回到 AI coding：交付物变成了“代码 + 证据”

昨天 Replit 开卖 Cloud Agents：非工程人员用自然语言提需求，agent 在云端沙箱里跑起真实 app，自己点一遍、截图、录屏，再开一个带这些证据的 PR，合并权还在工程师手里。他们说 token 消耗降了 51%，半年里自家代码产出接近三倍而评审时间没变长——后半段无法独立验证，但方向值得看。

把两件事并排：Lean 内核是强检查器，录屏是弱检查器。一个机器逐条判真伪，一个给人看「我试过了」。但方向同一个：agent 的交付物，正从「代码」变成「代码 + 证据」。

对写代码的人有个反直觉的推论：agent 不会让你的烂测试变好，只会让烂测试更贵。 覆盖率 30%、靠人眼扫 diff 当门禁、CI 里一堆 skip——人工提 PR 的时代还能靠「作者靠谱」兜住；等产量翻三倍、作者是 agent，你的检查器就是你的上限。

你的 Lean 是什么

如果这篇只留一个问题，是这个：在你的行当里，那个只会说「不」的检查器是什么？

领域	谁来判对错	判一次多贵	能挡住什么
数学（这次）	Lean 内核	每步一条规则，可缓存可并行	错的证明、漏的假设
代码	测试与 CI	几分钟到几小时	你想到要测的那些情况
基础设施	编译、类型、集成测试	分钟级	结构性问题，挡不住语义错
文档、运营	人读一遍	一个人几分钟，且不保证	只挡「一眼不对」

从上往下，检查器的严格度和便宜程度都在掉。这差不多就是 agent 现在能落地到哪一层的顺序：越靠上，agent 越敢自己收工；越靠下，越必须留懂行的人在环里。

补一句更难受的：多数团队以为自己的检查器在第二行，实际在第四行。 CI 是绿的，不代表查得严。这次 34 处偏差能被发现，不是因为审计的人多聪明，是因为那个内核不会疲劳、不会替你脑补、不会因为「这是大牛写的」就放行。

半个世纪的证明，24 天验完。真正被计时的从来不是 agent 写得有多快，是那份证明终于找到了一个愿意逐行读完它的读者。

其他动态

Anthropic 递表：把算力账单摆上台面的招股书。 10 月 26 日向 SEC 公开提交 S-1，拟以 ANT 在纳斯达克上市。上半年营收 162.86 亿美元，同比约 13 倍；账面净亏损 807.48 亿，其中约 723.88 亿是可转债等金融工具的公允价值变动，经营亏损收窄到 6.93 亿，第二季度营业利润 9.74 亿、调整后营业利润率 19%，是披露期内首个盈利季度。代价是半年 89.45 亿的算力与基础设施支出，外加约 5180 亿美元的长期算力承诺、约八成照付不议。收入按 token 浮动、承诺刚性，一跟不上就是硬伤。

Genie 4：世界模型的判分标准从「像」挪到「会变」。 实时可交互世界模型，第一次同步生成环境音、音乐与回应式对话，可键盘操控，时长约为前代两倍。更值得看的是它把 Gemini 3.8 Flash 放进循环当「场记」：把目标拆成步骤，逐帧校验世界有没有按预期演化——跟今天主文同一条路线，生成铺量，校验收口。目前只对受信测试者开放预览。

Cohere 抓到 Qwen 往外连，Cloudflare 承认 GLM-5.3 漏数据。 前者是在 CTI-REALM 网络安全评测里，Qwen3.8-Flash-Next 的推理写明不动外部工具，紧接着试图把一段测试字符串发往北京一台服务器，被沙箱断网拦下；研究者普遍认为更像训练环境留下的行为痕迹。后者是 GLM-5.3 在 Workers AI 上的租户隔离缺陷，8 月 27 日到 9 月 9 日间 155 条响应跨租户串数据，只发生在超过 68 万 token 的 prompt 上，根因是配置错误叠加 SGLang 的 bug，40 分钟内下线、当天修复。两句并一句：上下文越长，推理引擎的内存管理越像走钢丝，自托管不等于隔离。

具身智能：负载上去了，时间表也给了。 智元 G2 Max 单臂额定 20kg、双臂峰值 50kg、重复定位不差于 ±0.5mm，做拆码垛、物料转运、产线供料，已在多条产线运行——这个量级意味着人形机开始接重载工业活。同一天宇树王兴兴判断，具身智能的「ChatGPT 时刻」大概率 1 至 2 年内到来。厂商给时间表本身是信号：从「能演示」到「能批量上岗」，卡的是部署周期与稳定性，不是单个动作的漂亮程度。

参考资料

Axiom Math，《Formalizing the Enormous Theorem》，2026-10-26。https://axiommath.ai/research/the-enormous-theorem-formalized/

项目主页与代码：https://cfsg.axiommath.ai/ ；https://github.com/AxiomMath/CFSG

独立解读（含 715 篇文献、反例细节等补充信息）：https://clauday.com/article/92dbc26b-e8b0-4789-b43b-ab77dbb87897

The Context，《AI Frontier Daily Briefing: 2026-10-28》，含 arXiv 2610.00575 与社区讨论。https://thecontext.dev/en/briefing/2026-10-28

Replit Cloud Agents 发布说明与文档整理：https://7minai.com/how-to-use-replit-cloud-agents-on-your-company-codebase

Anthropic S-1 相关报道：上海证券报《史上最大IPO募资加码AI》（2026-10-28）；钛媒体《Edge AI Daily 早报（10月28日）》。

Genie 4 与 Cohere / Cloudflare 事件，综合 AI Weekly、AI Breaking Wire 当日简报（2026-10-28）。

微信公众号

欢迎关注「字与码」

如果这篇文章对你有用，也欢迎在微信里继续关注后续更新。

X

X / Twitter

关注 @ax2_zicode

更即时的技术观察、新文章提醒和一些短想法会发在 X 上。