Antigravity 的 /teamwork：多智能体把开放难题逐个拆开

📋 概述

Google Research 公布了 Antigravity 多智能体功能 /teamwork 的一批成果：与高校团队合作，把数学、化学、系统软件与机器学习工程里悬置多年的开放问题推进了一步。系统设计的两个出发点很具体——单次生成不可靠，于是并行探索并配「证伪器」（Lean 4 证明检查器、未改动的测试套件、模拟器、硬件计数器）自动筛掉错解；长任务里注意力会散，于是按构造切分上下文，每个专职智能体只拿到它那一步需要的文件与工具，评审者在干净上下文里复核，避免继承原作者的推理。文中列举了 Courtade–Kumar 猜想被完整证明并形式化为 5000 万行 Lean 代码，以及若干复杂度、量子查询与数据结构问题的突破。