谷歌近期扩展了 Antigravity 平台的 /teamwork 多智能体系统，由多个 Gemini 模型驱动的专业智能体分工协作，在数学与理论计算机科学方向完成了多项复杂证明的验证和形式化工作，包括韦伊猜想的端到端形式化、库尔塔德 - 库马尔（Courtade–Kumar）猜想的完整证明，以及三维纳维 - 斯托克斯方程有限时间爆破证明的形式化复现。这套系统的核心思路不是让单个大模型一口气写完长篇证明，而是把研究任务拆给并行工作的专业智能体，再安排独立的质疑者和审查者对结果交叉检查，以降低单模型在长链路推理中积累错误的概率。从公开成果看，Teamwork 已在信息论、代数几何、偏微分方程等方向产出可被机器检验的形式化结果，例如韦伊猜想形式化使用约 180 万行 Lean 代码、经历约 2.88 万次子智能体调用；库尔塔德 - 库马尔猜想的完整证明则在 Lean 4 中形成约 5000 万行代码。除数学外，同类多智能体编排方法也被尝试用于分子结构识别和软件代码重写，但本次公开的重点仍是数学证明与形式化验证方向。需要说明的是，这些 AI 协作成果均在人类专家参与下完成，形式化代码由定理证明器自动校验，最终学术结论仍以正式发表和同行评审为准；目前 Teamwork 已通过 Antigravity 对外开放，并计划为学术研究人员提供一定期限的免费访问额度。
一、系统基本定位
| 项目 | 内容 |
|---|---|
| 所属平台 | Google Antigravity |
| 系统名称 | /teamwork（Teamwork 多智能体框架） |
| 驱动模型 | Gemini 系列模型（公开材料涉及 Gemini 4 Argon、Carbon、Hydrogen 等） |
| 智能体形态 | 多个专业智能体并行分工，配合独立质疑者、审查者 |
| 典型模式 | Long Proof 长证明模式，底层对应 Stellar Colosseum 编排框架 |
| 校验工具 | Lean / Lean 4 定理证明器，对证明进行机器检查 |
| 协作方式 | 人类专家与 AI 智能体共同确定目标、审阅规范，智能体负责生成与迭代 |
二、数学方向代表性成果
| 成果 | 背景与方法 | 公开规模数据 |
|---|---|---|
| 韦伊猜想（Weil conjectures）形式化 | 关于有限域上多项式方程解数量的经典结论，原始证明由德利涅于 1974 年完成；Teamwork-LEAP 端到端自主生成机器可检查的形式化 | 约 180 万行 Lean，2.88 万次子智能体调用 |
| 库尔塔德 - 库马尔猜想（Courtade–Kumar conjecture） | Google、CUHK、USC、CMU 团队协作，使用 Long Proof 模式完整证明信息论猜想；Gemini 先找到早期广义猜想的反例，团队提出新候选函数并归约为 14 变量优化问题，模型再划分参数空间、推导解析界与区间算术证书，并把证明从平衡函数扩展到非平衡函数 | Lean 4 形式化代码约 5000 万行 |
| 希尔伯特第十问题（一般整数环）证明形式化 | 对一项近期证明完成首次形式化，合成超过 91.9 万行 Lean | 超 91.9 万行 Lean |
| 三维纳维 - 斯托克斯方程有限时间爆破证明复现 | 端到端复现光滑强迫条件下有限时间爆破证明的形式化；该问题属于千禧年难题相关方向，已开放约 90 年 | 公开材料未单列代码规模 |
三、多智能体协作与验证机制
1. 分工与并行
- 项目协调智能体把复杂任务分派到不同并行工作流，每条工作流由对应协调智能体管理。
- 专业智能体只被授予完成当前任务所需的文件和工具访问权限，缩小操作范围。
- 候选证明并行生成，再经过定向证伪和交叉质疑，有效结果汇入可复用的验证结果台账。
2. 独立质疑与审查
- 审查环节由独立于原始生成智能体的质疑者、审查者承担，不依赖生成方自己的推理过程。
- 这种 "生成 — 质疑 — 复核" 的回路，用于减少单模型在长程推理中前后矛盾、弱化定理陈述或引入漏洞的风险。
- 形式化结果最终交由 Lean 定理证明器自动检查，研究者主要在运行前审阅问题规范。
3. 长证明编排逻辑（Stellar Colosseum）
- 证明构建前先探索多种备选策略。
- 通过就绪门槛（readiness gate）判断某条路线是否成熟到可以分解。
- 证明计划表示为相互依赖的小节级子问题，验证发现的问题回流到论证的对应部分。
- 多轮候选与批评意见通过重叠随机采样树聚合为统一研究产物。
四、其他方向的延伸应用（公开简况）
- 分子化学：由 30 个专业智能体配合融入物理知识的模拟器，基于核磁共振（NMR）数据识别分子结构；复杂分子基准测试中 Top-1 准确率 95%，Top-3 准确率 100%。
- 软件工程：智能体团队将 libgav1 AV1 视频解码器由 C++ 重写为 Rust，生成约 17 万行代码，覆盖测试中输出结果与原版一致。
- 上述方向属于同一多智能体编排能力的延伸演示，与数学证明成果分属不同评测场景，不宜直接横向比较指标。
五、开放使用安排
- 谷歌已通过 Antigravity 对外开放 Teamwork 系统，以及名为 /boost 的迭代式编程工作流。
- 公开计划显示，将面向 1 万名学术研究人员提供为期 6 个月的最高使用额度免费访问。
- 具体接入条件、可用模型和额度规则以 Antigravity 官方最新说明为准。
【常见问题】
问题 1：谷歌 Teamwork 系统是什么，由哪些专业 AI 智能体和模型构成？
回答 1： Teamwork 是谷歌 Antigravity 平台上的多智能体编排框架，由多个 Gemini 系列模型驱动的专业智能体组成，配套独立的质疑者和审查者角色；系统包含 Long Proof 长证明模式，底层对应 Stellar Colosseum 框架，证明结果通过 Lean 定理证明器做机器检查。
问题 2：Teamwork 系统在复杂数学证明方面验证了哪些代表性成果？
回答 2： 公开成果包括韦伊猜想的端到端形式化（约 180 万行 Lean、2.88 万次子智能体调用）、库尔塔德 - 库马尔猜想的完整证明（Lean 4 约 5000 万行代码）、一般整数环希尔伯特第十问题近期证明的首次形式化（超 91.9 万行 Lean），以及三维纳维 - 斯托克斯方程有限时间爆破证明的形式化复现。
问题 3：Teamwork 多智能体架构如何减少长篇推理过程中可能出现的错误？
回答 3： 系统让专业智能体并行生成候选方案，每个智能体只能访问任务所需的文件和工具；随后由独立于生成方的质疑者、审查者交叉检查，不依赖原始智能体的推理过程；形式化结论再交 Lean 自动校验，配合就绪门槛、子问题分解和验证结果回流机制，降低单模型长链路推理累积错误的概率。
问题 4：这套 AI 智能体系统除数学证明外还有哪些应用，目前如何开放使用？
回答 4： 同类编排能力还被用于分子结构识别（30 个智能体配合物理模拟器分析 NMR 数据，复杂分子基准 Top-1 准确率 95%、Top-3 为 100%）和软件代码重写（libgav1 解码器 C++ 转 Rust，约 17 万行代码）；Teamwork 与 /boost 工作流已通过 Antigravity 开放，并计划为 1 万名学术研究人员提供 6 个月最高额度免费访问。
【参考资料】
- [2026-11-14]（谷歌利用多个专业 AI 智能体打造 Teamwork 系统，成功验证多项复杂数学证明）IT 之家（今日头条转载）
- [2026-11-13]（Advancing science & engineering with Antigravity's /teamwork）Google Research 官方博客
- [2026-11-14]（谷歌利用多个专业 AI 智能体打造 Teamwork 系统，成功验证多项复杂数学证明）凤凰网科技
- [2026-09-07]（谷歌让 AI 互怼几天，小模型竟复现 3 道博士级难题）36 氪
- [2026-08-31]（Gemini Multi-Agent Teams in Antigravity）Google Blog
- [2026-09-30]（Stellar Colosseum: A Many-Agent Harness for Long-Horizon Research in Mathematics and Theoretical Computer Science）arXiv
【免责声明】
本文内容整理自公开媒体报道与谷歌官方博客，仅供技术与行业信息参考，不构成学术评价、软件选型或科研决策建议。文中数学证明与形式化结果的最终有效性以正式同行评审论文和定理证明器复核记录为准；AI 辅助产出的结论需经人类专家审查，模型能力、调用规模和开放政策可能随版本更新调整。