AREX Feed Article
Google 自称 Teamwork 解决 7 个开放数学问题，Knuth 循环猜想经 Lean 验证
8 月 27 日，Google Antigravity 官方博客发布长文，宣布多智能体编排框架 Teamwork 的多项更新。最重的一项声明是：官方自称 Teamwork 解决了 7 个数学与理论计算机科学开放问题，其中包括 Knuth 的循环猜想——偶数情形两个更简单构造的首批证明，40 页证明经 Lean 形式化验证。
同一篇博客还给出 TCSBench 71% 的组合得分（Gemini 3.7 Flash 搭配 3.1 Pro，官方称内部测试最高）、一台从零构建、能启动 xv6 的周期级乱序 RISC-V 模拟器，以及合入 Eigen 与 ParlayHash 上游的优化。这些均为 Google 自报结果：除 Lean 验证的 Knuth 证明外，其余结论的验证依赖官方所称的人类专家审核。
七个开放问题：六项人审，一项 Lean 验证
博客列出的七项结果，覆盖 FOCS 2025、JMLR 2021 等会议期刊上的开放问题，也包含工程向问题。
第一项是 ℓ_p 子空间逼近的 Coresets（FOCS 2025 开放问题）。对应论文 于 8 月 26 日上传，作者为 Honghao Lin、Vahab Mirrokni、David P. Woodruff，摘要称把 Woodruff–Yasuda 在 FOCS 2025 得到的 coreset 规模界改进为 Õ(kε⁻²) 和 Õ(k^{p/2}ε⁻²)。第二项稀疏凸优化（JMLR 2021 的 Axiotis–Sviridenko 猜想）对应 ，对稀疏最小二乘建立了条件性下界。第三项最大内积嵌入（Jayaram 2026 开放问题）对应 ，几乎闭合了 Chamfer 相似度的复杂度间隙。第四项可证明的 Hadamard 量化（Feng 等 2026 开放问题）对应 ，消除了第二量化阶段，前导常数降约 5.93 倍。
第五项是 Erdős 单位距离问题，官方称独立复现了单位距离指数的初始突破，且"在没有网络访问的情况下重新发现了解法"。第六项前缀矩阵分解（Bulanek 等 2026 开放问题）对应 ，给出近最优下界。第七项即 Knuth 循环猜想：偶数情形两个更简单构造的首批证明，40+ 页与 70+ 页各一份，其中 40 页证明经 Lean 形式化验证。
验证口径要分清。博客称，除 Knuth 循环猜想外，其余结果"已经人类专家审核并确认正确"；Knuth 那一项走的是 Lean 机器验证而非人审。七项中五篇论文已上传 arXiv，均可从 arXiv 页面直接查看。其中四篇（2608.02588、2607.20393、2608.02564、2608.08238）的摘要写明：证明最初由 Google 内部开发的、基于 Gemini 的自动化智能体系统获得，作者随后人工核验并整理成文。这是对"智能体做研究"叙事的第二处佐证，但核验者仍是论文作者本人。
官方还披露了两个边界：这些结果由 Gemini 3.1 Pro 完成，其中第 1、3、4 项用 Gemini 3.7 Flash 复现，官方称这是 Flash 级模型首次产出博士级数学研究；部分结果使用了高于默认的并行度，Antigravity 上开放版本在成本与能力之间做了取舍。
Knuth 的 "Claude's Cycles"：偶数情形此前悬而未决
Knuth 循环猜想为什么值得注意，要先说明它的出处。它来自 Knuth 2026 年的论文 "Claude's Cycles"：顶点集为 (Z/mZ)³ 的有向 Cayley 图，每个顶点沿三个坐标方向各有一条出边，问题是要把所有有向边分成三条两两边不相交的有向哈密顿圈。
据 ：Knuth 给出了显式规则 σ_Knuth，并声称它对所有奇数 m≥3 成立；偶数情形一般地悬而未决，m=2 已知不可能（Aubert–Schneider，1982）。issue 作者还写道，Knuth 借助 Claude 的帮助解决了他思考数周的问题，这解释了猜想名字的由来。该 issue 把偶数情形列为开放问题，并征集 Lean 形式化。Google 博客声称的"首批证明"，针对的正是这一情形。
TCSBench 71%：每个候选策略都配一名专职证伪者
Long Proof 是 Teamwork 面向开放式数学研究的模式，设计上不靠单一更大模型，而靠协调大量 agent。其核心机制是竞争式策略搜索：并行生成多个候选策略，每个候选配一个专职证伪者（falsifier）负责拆台；合成树把候选与证伪报告组合，被推翻的路径不删除，而是带着反对意见留在流程里，因为一条走不通的路可能仍含有可用的想法。
选中策略后，框架把它展开成带显式依赖关系的证明计划，独立子问题并行执行；每个子问题还有自己的 tournament 网络，合成结果失败就带着累积的反对意见重跑。失败草稿留给下一轮，证伪结论沉淀进与答案无关的"陷阱登记册"（pitfall registry），共享知识目录记录已证结果、失败方法与参考。
基准方面，官方称用 Gemini 3.7 Flash 搭配 3.1 Pro，Long Proof 模式在 TCSBench 上拿到 71%。TCSBench 是 Google 内部独立开发的 TCS 评测集；此前 TCSBench 论文报告 Gemini 3.6 Flash + 3.1 Pro 为 67.7%。71% 被官方称为"内部测试最高"。Flash 与 Pro 在 Long Proof 中的组合能力，将在后续更新中开放。
Teamwork 的模式不止数学。官方称调用 /teamwork-preview 时，Gemini 先分析提示词、自动挑选模式；编排逻辑与 agent 描述解耦，模式只是规格说明，框架按任务动态决定 agent 数量与轮数，团队结构可在运行中途变化。已内置 Iterative Coding、Distributed Coding、Long Proof、Self-Verification（受今年早些时候公布的 Aletheia 智能体启发）、Document Review 五种模式。
从零写一台能启动 xv6 的乱序 RISC-V 模拟器
系统工程的例子是一台周期级乱序（out-of-order）RISC-V CPU 模拟器。官方称用 Gemini 3.7 Flash 驱动 Teamwork 从零构建，模拟器成功把 xv6 操作系统启动到 shell，并跑过 100 多个 RISC-V 标准基准。
过程分两阶段。先做微架构功能正确性：乱序流水线与重排序缓冲（ROB），对照功能 oracle 保证架构状态正确、能启动操作系统。再做周期级时序验证：把周期数与气隙部署的 Boom 模拟器对齐，微架构单元（MSHR、ROB、Cache 等）由 agent 自行构建并通过微基准验证。与 BOOM 硬件执行真值对照，未见过的测试负载上平均周期对齐误差 0.71%。
难点被官方称为"静默执行间隙"：微架构状态可能先悄悄偏离最多数百个周期，直到架构级失败才显现。为防止模拟器作弊，Spike 模拟器源码被沙箱隔离；Teamwork 的方案是与气隙 Spike 参考模拟器持续 lockstep 协同模拟，让偏离在数百个周期内暴露。
合入 Eigen 与 ParlayHash 上游的两笔提交
开源侧的成果可以直接检查。针对线性代数库 Eigen，Teamwork 发现 GeMV 操作在矩阵只有单行或单列时的次优实现，建立了一条专用快速路径：直接数据访问加 SIMD，配 4 路累加器展开。该改动经标准开源评审流程合入 Eigen 上游，评审过程由 Gemini 3.6 Flash 辅助。
并发哈希表 ParlayHash 方面，Teamwork 参与了 Swiss Parlay 的构思，把 Swiss Table 的优化引入 ParlayHash：64 线程下初始插入吞吐 2 倍，单线程整体吞吐 1.5 倍，接近顺序表最优实现 FlatHashMap 且每元素内存少 25%，改动已落入上游分支。博客强调："这些不是只存在于基准里的结果，而是经外部维护者通过标准开源评审接受的真实贡献。"
自报结果的验证边界
可确认的事实层面：Teamwork 首次公布于 Google I/O，官方称其能力建立在 Gemini 3.7 Flash 发布之上；/teamwork-preview 已对所有付费计划开放，官方称未来几周陆续推送新能力。官方对 Teamwork 的定位是压缩"深度专家花数月完成"的迭代周期，同时让专家保留方向与验收权。
验证层面则不同：71% 是"内部测试最高"，不是第三方榜单；六项数学结果依赖官方所称的人类专家审核。对外的检验通道是这五篇 arXiv 论文和 GitHub 上的解法代码，其中只有 Lean 验证的 40 页证明属于机器层面的严格验证。