Google Research 副总裁、Google Fellow Vahab Mirrokni 11 月 13 日发文，把 Antigravity 里的多智能体工作流 /teamwork，连同 /boost 和 Deep Review，向外部的研究者和开发者开放。博文同时汇总了过去几周里，Google 与学术合作者使用 Gemini 4 和这套工作流得到的一批数学、化学和系统工程结果。
这两件事要分开看。工具开放是 13 日的新动作；成果清单里既有人机合作的新证明，也有对已有证明的机器检查形式化，其中最完整的一篇数学论文 9 月就已经挂上 arXiv。
外部现在能用到哪一步
Antigravity 文档写明，/teamwork 在付费方案里可用，覆盖应用和命令行。它把长任务拆成里程碑，由 Sentinel 和 Project Orchestrator 调度只读的 Explorer 与负责改代码的 Worker，再经过 Critic、Challenger、Auditor 和 Success Auditor 这些独立检查关口。文档把它定位在持续数小时到数天的多里程碑项目上，例如仓库级迁移、系统仿真或形式化证明。更短、更局部的任务，文档建议改用 /boost、/swarm 或普通子智能体。
Mirrokni 的博文从设计动机上补了两句。一层是给候选答案配上可自动执行的验证器，例如 Lean 4 证明检查器、未改动的测试套件、执行仿真或硬件计数器。另一层是按任务切开上下文：每个专门智能体只拿到完成这一步所需的文件和工具，协调者会把任务交给新的后继者，评审方则在干净的上下文里检查，不带着原作者的推理过程。
博文还说，公司已开放申请，向 1 万名学术研究者提供最高用量档半年免费使用。形式化证明所用的专用模式，以及其他一些专门工作流，要到随后几周才会进入 Antigravity。申请入口和审核规则，博文没有展开。
Courtade–Kumar 猜想：论文在 9 月，仓库可以公开检查
博文里着墨最多的新证明，是信息论中的 Courtade–Kumar 猜想，也叫“最有信息量的布尔函数猜想”。它问的是：随机比特串经过噪声信道后，有没有哪种把输入压成一个比特的办法，能比只复制其中某一位保留更多信息。猜想认为没有，极值由所谓的独裁函数取到。
对应论文是 arXiv:2609.24931，题为 A Proof of the Most Informative Boolean Function Conjecture。作者是 Zijie Chen、Amin Gohari、Adel Javanmard、Honghao Lin、Vahab Mirrokni、Chandra Nair 和 David P. Woodruff，分属香港中文大学、Google、南加州大学和卡内基梅隆大学。arXiv 记录的首个版本提交于 2026 年 9 月 21 日，修订版在 9 月 24 日上线。
博文对分工的说法是：Gemini 先找到了中大团队早前一篇论文里某个推广猜想的反例；中大团队随后提出一个候选函数，把原猜想收成 14 个变量的优化问题，并给出关键的分析下界；Gemini 4 Argon 和更早的 Gemini 模型再剖分参数空间，完成了大部分新的分析界和区间算术证书，还在没有人工介入的情况下，把证明从平衡函数扩到了非平衡函数。这些步骤目前主要来自 Google 的叙述。论文本身写的是一篇有计算机辅助步骤、并在 Lean 里做了端到端核验的证明，同时也记录了独立工作：Vu Khac Ky 与 Tuan Tran 有一份方法不同的证明，两边协商后同期挂上 arXiv；之后另有小组联系作者，分享了各自的稿件或提纲。
公开的 Lean 仓库是 David P. Woodruff 维护的 general-courtade-kumar-lean，创建于 9 月 24 日。仓库里的 formalization.yaml 写明，这是对上述论文主定理的完整 Lean 4 形式化，声明为 GeneralCK.ArchiveRegionalBoundary.generalCourtadeKumar_closed，sorry 数量为 0，只依赖 Lean 的三条标准公理。仓库共有 4.55 万个 Lean 源文件，其中大部分是交给 Lean 内核检查的生成数值证书。README 给出了复现路径，并估计完整构建大约需要 1200 个 CPU 小时。同一陈述还在 10 月 15 日并入了 Google DeepMind 的 Formal Conjectures 仓库。Google 博文里“约 5000 万行 Lean 代码”的说法，公开仓库的元数据没有给出可与之对应的行数，本文不以这个数字为准。
其中多项工作是对已有证明的形式化
博文后半部分把另一类工作放在 LEAP 框架下：从非形式化的证明出发，生成可被 Lean 内核逐行检查的形式化文本。这里的贡献是把已有证明变成机器可复核的代码，不是重新证明这些定理。
Weil 猜想是其中篇幅最长的一项。博文写的是对 Pierre Deligne 1974 年证明的端到端形式化，约 180 万行 Lean，调用了 2.88 万次子智能体。三维 Navier–Stokes 方程那一项，写的是对“带平滑外力的三维方程存在有限时间 blowup”这一近期证明的形式化。它属于千禧年大奖问题的附近，但并不是通常所说的、无外力的三维 Navier–Stokes 正则性问题本身。这些行数和调用次数目前只有博文口径，尚未见到对应的公开仓库。
同一清单里还有对一般整数环上希尔伯特第十问题近期证明的形式化、对 Birkhoff 猜想和三维 Bochner–Riesz 猜想的首次形式化等。博文称，在后一项中，系统还发现并修补了近期非形式化证明里的一处缺口。这些结果同样有待公开仓库或论文来交叉核对。
Deep Review 被写成 /teamwork 的文档审阅模式，现在也可以在 Antigravity 里使用。博文称，在 STOC 2027 投稿中，有 578 篇、超过三分之一的稿件选择接受反馈；一份仍在进行、样本为 70 人的作者调查里，90% 的受访者认为反馈大部分或几乎全部属实。这是公司公布的调查，不是第三方评估。
工程和生产数字目前只有公司口径
博文还列出了一组系统工程和内部生产结果。例如用 /teamwork 和 Argon 做的 FarArray 内核旁路地址空间、9×9 围棋引擎的自我对弈优化、把 Zircon 微内核剩余的 C++ 代码改写成约 80 万行通过测试并可在 arm64 上启动的安全 Rust，以及把 libgav1 解码器改写成约 17 万行、在一致性测试上逐比特一致的 Rust 实现。生产侧则提到，机群内存优化找到的节省机会已超过最初估计的 1 PiB；Borg 的调度工作流上线了两项改动，在部分硬件上把 TPU 任务抢占降低了 24%。
这些数字都来自 Google 自己的测试或内部部署，目前没有独立复现。化学结构解析里“复杂基准分子上 top-1 精确匹配 95%”的成绩，同样只是博文自述。
对外部用户来说，13 日能确认的是：付费方案里可以用 /teamwork 和 /boost，Deep Review 也已开放；数学上至少有一篇 9 月就公开的 Courtade–Kumar 证明，并带有可检查的 Lean 仓库。其余成果要按“新证明、对已有证明的形式化、公司自测”分开读。形式化证明的专用模式何时完全对外部开放，仍要等 Google 接下来几周的更新。
