谷歌让一群 Gemini 智能体组队：写出 180 万行 Lean 代码，证明韦伊猜想

谷歌把旗下的 Antigravity 多智能体系统又往前推了一步，用多个 Gemini 驱动的专业智能体组成 Teamwork，目标很硬：解决长期悬而未决的数学难题、验证复杂证明，顺带优化软件性能。

已经拿出的成绩单包括韦伊猜想的形式化证明。这组关于有限域上多项式方程解数量的结论，最早由德利涅在 1974 年证明；Teamwork-LEAP 系统调用了约 2.88 万次子智能体，累计生成约 180 万行 Lean 代码，才把这项工作形式化完成。团队还复现了三维纳维-斯托克斯方程有限时间爆破问题的一项形式化证明，并帮助研究人员解决了库尔塔德-库马尔猜想。

做法上，多个智能体并行开工，另有一套独立系统专门挑错、验证答案，降低单个模型长篇推理时跑偏的概率。每个专业智能体只能碰完成任务所需的文件和工具，结果交给独立的质疑者和审查者检查，不依赖原智能体的推理过程。

数学之外，谷歌也把这套东西用到分子化学：30 个专业智能体配合融入物理知识的模拟器，靠核磁共振数据识别分子结构，复杂分子基准上 Top-1 准确率 95%，Top-3 达到 100%。系统工程方面，智能体团队把自家 libgav1 AV1 视频解码器从 C++ 重写成 Rust，产出约 17 万行代码，测试输出与原版完全一致。

目前 Teamwork 和名为 /boost 的迭代式编程工作流已通过 Antigravity 向用户开放，谷歌还计划给 1 万名学术研究人员提供 6 个月最高额度免费访问。