谷歌用多个专业智能体组成 Teamwork 系统，完成韦伊猜想形式化证明

谷歌宣布扩展 Antigravity 多智能体系统，推出由多个 Gemini 驱动的专业智能体组成的 Teamwork 系统，用于解决复杂数学问题并验证形式化证明。其中 Teamwork-LEAP 系统通过约 2.88 万次子智能体调用、累计生成约 180 万行 Lean 代码，完成了韦伊猜想（Weil conjectures）的形式化证明，该猜想最初由数学家德利涅于 1974 年证明。系统还复现了三维纳维-斯托克斯方程有限时间爆破问题的形式化证明，并帮助解决了库尔塔德-库马尔猜想。 技术架构上，Teamwork 依靠多个智能体并行工作，每个专业智能体只能访问完成任务所需的文件和工具，再由独立的质疑者和审查者检查结果，不依赖原始智能体的推理过程，以降低长篇推理中的错误率。除数学外，谷歌将这套方法用于分子化学：30 个专业智能体配合融入物理知识的模拟器，基于核磁共振（NMR）数据识别分子结构，在复杂分子基准测试中 Top-1 准确率达 95%、Top-3 达 100%。 在系统工程方面，智能体团队将谷歌自家的 libgav1 AV1 视频解码器从 C++ 重写为 Rust，生成约 17 万行代码，并在广泛测试中实现与原始版本完全一致的输出。谷歌目前通过 Antigravity 开放 Teamwork 系统和 /boost 迭代式编程工作流，计划向 1 万名学术研究人员提供为期 6 个月的最高额度免费访问。