一句话：谷歌没有证明韦伊猜想，它只是把 1974 年已经完成的证明搬进了机器，并且让机器能逐行复核。
据 IT 之家 11 月 14 日报道，Google Research 在 11 月 13 日公布：Antigravity 的 /teamwork 多智能体工作流，由 Gemini 4 的 Argon、Carbon、Hydrogen 驱动，配合高校合作，在形式化验证、信息论、内核优化等方向拿出了一批结果。数字很震：约 180 万行 Lean，2.88 万次子智能体调用。但先别被数字晃了眼，我们先把事情说清楚。
形式化到底是什么活
韦伊猜想是关于有限域上多项式方程解的数量的结论，1974 年德利涅完成关键证明，拿了菲尔兹奖。谷歌这次做的不是新证明，是形式化：从非形式化证明出发，把它写进 Lean，让机器逐步检查。证明的原创性属于 1974 年，机器做的是复核。
形式化还有个不那么浪漫的副作用：它逼着你把模糊的地方说死。「显然易得」「不难证明」这类话在论文里通行，在 Lean 里等于没写。180 万行代码里，每一处省略都得补全，证明的粗糙之处会原样显形。
这活不好干。Lean 现有的数学库庞大，陈述要和对齐现有定义，改一个字都可能编译不过。180 万行代码不是「AI 写出来」那么简单，而是 AI 和检查器之间反复拉扯、来回修改的过程，机器检查器那边从来不讲情面。
对数学家来说，形式化证明还有个副产品：一份可以直接查错的文本。过去同行评审挑出的错误靠运气，现在把证明喂给 Lean，错的步骤会被编译器逐条点出来。谷歌这次顺手修复了近期非形式化证明里的一个缺口，正是这个机制的自然产出。
180 万行 Lean 怎么来的
划重点：这不是一个模型坐下来写完的。按谷歌的口径，Teamwork-LEAP 从非形式化证明出发，通过多智能体协作流程，端到端完成形式化，直到 Lean 内核认账，机器检查通过。交出来的是一份能编译的代码库，不是一篇论文。
谷歌管这个叫「多智能体工作流」，Gemini 4 的 Argon、Carbon、Hydrogen 三个档位分工。这次任务里总共 2.88 万次子智能体调用。算下来这是一条流水线，不是个人英雄主义，单点模型的可靠性被摊薄到了流程上。
其他成果还有：CUHK、USC、CMU 的 Courtade–Kumar 猜想一般情形约 5000 万行 Lean；91.9 万行完成一般整数环上希尔伯特第十问题近期证明的首次形式化；Birkhoff 猜想（1927 年悬置）和三维 Bochner–Riesz 猜想（悬置 50 余年）也首次形式化。
数字很震，但要保持冷静：行数全是谷歌口径，本身不说明难度——翻译已有证明和原创证明是两个量级，谷歌做的全是前者。化学方向同理：30 个专业智能体团队靠物理模拟器和核磁共振数据识别分子结构，复杂分子基准 Top-1 准确率 95%、Top-3 100%，同一套机制换了学科。
真正的突破是「把反对制度化」
机制设计对着大模型两个短板：单次生成不稳定，长任务丢细节。谷歌的回应是给「反对」建系统——不是让模型更靠谱，而是设一批不依赖模型的反对者。模型负责生成，外部裁判负责是否签收。
第一层，配对并行探索加专门的「证伪者」：Lean 4 证明检查器、未修改的测试套件、执行仿真器、硬件计数器，全都站在模型外面。它们不可说服，不可谈判，不接受解释——错了就是错，没有中间地带。
第二层，按构造切割上下文：每个专业智能体只能拿到当前步骤需要的文件和工具，协调者把任务交给全新的后继者，审查者从干净上下文重新检查。审查者看不到作者的辩解，看不懂就毙，想参考前人的思路都没有入口。
说白了，过去「AI 写代码」的价值在生成，现在的价值在验证比生成更可信。生成那边永远可以重跑，验证那边一旦放水，整条链就废了。Teamwork 的内核其实是：不相信自己。
但这里有个前提
第一，Lean 编译通过不等于「形式化陈述和数学家原意一致」。谷歌自己也承认，陈述的匹配需要人类确认。所以最后一道闸还是人，只是从审证明挪到了审陈述，工作量小一点，分量更重。
第二，成本和可维护性没公布。2.88 万次调用烧了多少 Token？180 万行 Lean 的模块结构、编译资源、依赖版本、能回馈现有数学库的比例，第三方（openai-hub 等）都指出了这些空白。这些数字不补齐，性价比算不了，复现也无从下手。
第三，相对乐观的一点：谷歌把 Antigravity 的 /teamwork、/boost、Deep Review 开放给外部研究者，并向 1 万名学术研究者提供 6 个月最高档免费访问的申请通道。意味着你不信谷歌的口径，可以自己去跑、去查。开放性是对冲「没公布」的唯一办法。
质疑式收尾：这份答卷工程上打 A，透明度上打 C。数字很震，但真正值得研究的是那套机制——把反对做成制度。至于 180 万行代码别人能不能独立审下来，等开源社区的回复。
