谷歌用多个专业智能体组成 Teamwork 系统，完成韦伊猜想形式化证明
谷歌利用多个专业 AI 智能体打造 Teamwork 系统，成功验证多项复杂数学证明
谷歌把 Gemini 拆成分工不同的智能体团队，写 Lean 证明、重写 Rust 解码器、识别分子结构都跑通了，还有独立审查者专门挑错。做形式化验证或大型代码迁移的开发者值得关注，现在还能申请 6 个月免费额度。
谷歌宣布扩展 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 个月的最高额度免费访问。
谷歌利用多个专业 AI 智能体打造 Teamwork 系统，成功验证多项复杂数学证明
IT之家 11 月 14 日消息，谷歌宣布进一步扩展旗下 Antigravity 多智能体系统，利用多个由 Gemini 模型驱动的专业智能体组成 Teamwork 系统，号称可解决“长期悬而未决的数学难题”、“验证复杂数学证明”，并优化各种软件系统性能。 例如，谷歌已成功对韦伊猜想（Weil conjectures）进行形式化证明。这是一组关于有限域上多项式方程解的数量的重要数学结论，最初由数学家皮埃尔 · 德利涅（Pierre Deligne）于 1974 年证明。谷歌 Teamwork-LEAP 系统通过约 2.88 万次子智能体调用，累计生成约 180 万行 Lean 代码，完成了相关数学成果的形式化工作。 谷歌还表示，相应系统近期还成功复现了一项关于三维纳维-斯托克斯方程（Navier–Stokes equations）有限时间爆破问题的形式化证明。并帮助研究人员解决了库尔塔德-库马尔猜想（Courtade–Kumar conjecture）。 从技术层面，谷歌 Teamwork 系统主要依靠多个智能体并行工作，并安排独立系统对提出的解答进行质疑和验证，以减少单个 AI 模型在生成长篇推理过程中可能出现的错误。每个专业智能体只能访问完成任务所需的文件和工具，随后由独立的质疑者和审查者检查结果，而不依赖原始智能体的推理过程。 除了数学研究，谷歌还将这套技术应用于分子化学领域。一支由 30 个专业智能体组成的团队，配合融入物理知识的模拟器，利用核磁共振（NMR）数据识别分子结构。在复杂分子基准测试中，该系统的 Top-1 准确率达到 95%，Top-3 准确率达到 100%。 在系统工程领域，谷歌也展示了多智能体协作的应用成果。该公司表示，其智能体团队将自家的 libgav1 AV1 视频解码器从 C++ 重写为 Rust，最终生成约 17 万行代码，并在一套覆盖范围广泛的测试中实现了与原始版本完全一致的输出结果。 目前，谷歌正通过 Antigravity 向用户开放 Teamwork 系统，以及名为 /boost 的迭代式编程工作流，计划向 1 万名学术研究人员提供为期 6 个月的最高使用额度免费访问权限。
This report is categorized under AITOP's "Products" desk, focusing on US frontier AI labs and Silicon Valley technology leaders. Within our cross-regional analytical framework, it directly maps to AI developer toolchains, coding agents, and engineering workflows. Key entities and technical topics under continuous tracking include Gemini, Antigravity, multi-agent systems, formal verification.
Source attribution: curated from IT之家.
