谷歌将Antigravity扩展为多智能体Teamwork，2.88万次调用形式化韦伊猜想
谷歌于 11 月 14 日宣布将 Antigravity 扩展为多智能体「Teamwork」系统：多个由 Gemini 驱动的专业智能体并行工作，各自只能访问完成任务所需的文件和工具，再由不依赖原始智能体推理过程的独立质疑者和审查者检查结果，以减少长篇推理中的错误。公司自述的数学成果包括：Teamwork-LEAP 通过约 2.88 万次子智能体调用、累计生成约 180 万行 Lean 代码，完成韦伊猜想的形式化——该猜想 1974 年已由德利涅证明，此举属于对已有成果的形式化而非新数学发现；此外还称复现了三维纳维-斯托克斯方程有限时间爆破问题的形式化证明，并协助研究人员解决了库尔塔德-库马尔猜想。应用侧的自报结果还有：30 个专业智能体配合融入物理知识的模拟器，用核磁共振数据识别分子结构，复杂分子基准 Top-1 准确率 95%、Top-3 准确率 100%；以及将 libgav1 AV1 视频解码器从 C++ 重写为约 17 万行 Rust 代码，测试输出与原始版本一致。谷歌正通过 Antigravity 开放 Teamwork 与 /boost 迭代式编程工作流，计划向 1 万名学术研究人员提供 6 个月最高额度免费访问；上述数字与成果均为公司自述，来源为 IT 之家转述，独立验证情况不明。
rss · IT之家 · 11月14日 06:53
「为何现在值得关注」 这是谷歌当日刚公布的系统扩展，属于「多智能体分工 + 独立质疑验证」架构在形式化数学和系统工程上的具体落地，热度期内适合解读。但需要把两层区分开：已经发生的是公司对系统架构和成果的宣布，而 Lean 代码是否公开可复核、基准是否经第三方验证均未证实。
「内容切入角度」 可做角度：拆解 Teamwork 的「专业智能体分工 + 独立质疑者审查」架构为何有助于控制长推理的错误，并厘清这批成果的定性——它们是对已证明数学结论（如 1974 年已证的韦伊猜想）的形式化与复现，而非 AI 的新数学发现，同时指出约 180 万行 Lean 代码、95% Top-1 等关键数字目前均为谷歌自报，尚待公开可复核的独立验证。
做AI项目，先看AI雷达 - AiRadar.com.cn · 全部AI快讯 →