Gemini多代理解出7道开放题：证明可核验，成绩仍属内部测试

Google于2026年8月31日发布的成果摘要 显示，Gemini模型与Antigravity Teamwork组成的多代理系统处理了7项开放数学及理论计算机科学问题，并在内部TCSBench测试中取得71%。同一项目还展示了RISC-V处理器模拟器以及进入开源项目上游的性能优化。

这些结果的证据强度并不相同：Lean形式化证明、预印本和公开代码可以由外部人员逐项检查，TCSBench百分比及硬件对齐误差则仍来自项目方的测试环境。一份独立的逐项核查 找到了5篇预印本、Lean验证产物和两项上游代码改动，但没有找到TCSBench或处理器实验的外部复跑结果。

七项成果涵盖新证明、改进和独立复现

Antigravity团队8月27日的完整技术说明 列出七项结果，并注明它们最初由使用Gemini 3.1 Pro的Teamwork运行获得；其中第1、3、4项后来由Gemini 3.7 Flash复现。因此，“解出7道开放题”描述的是Gemini模型与Teamwork编排构成的整体系统，不能改写为3.7 Flash独立首次完成全部七项。

• ℓp子空间近似：针对p大于2的情形改进coreset构造界，对应FOCS 2025提出的问题。
• 稀疏凸优化：为稀疏最小二乘目标的条件数给出依赖特定复杂性假设的下界。
• 最大内积与Chamfer嵌入：进一步缩小单向量与多向量嵌入之间的复杂度差距。
• 可证明Hadamard量化：去掉第二次量化阶段，并改善理论分析中的主导常数。
• Erdős单位距离问题：在不能联网的条件下重新获得一项已有突破，属于独立复现而非首次发现。
• 前缀矩阵分解：给出接近最优的下界。
• Knuth Cycles猜想：为偶数情形的两个较简单构造给出首批证明，其中一份超过40页的证明完成Lean形式化验证。

七项工作的研究性质并不统一：有的是新界或新证明，有的是条件性结论，也有一项是对既有成果的重新发现。这个计数可以说明系统覆盖的任务数量，却不能证明七项结果都已成为经过同行评议的新定理。

Lean证明、预印本与上游代码不是同一级证据

Lean证明提供的是形式正确性检查。证明检查器能够逐步判断推导是否符合声明的规则和前提，因此比仅有自然语言论证更容易独立复核。不过，形式验证不会自动判断研究问题的重要性，也不能替代对问题设定、假设和学术贡献的同行评议。

五项结果已有arXiv预印本，外部研究者可以检查定义、假设和推导。稀疏凸优化论文在文本中记载，证明最初由自动化Gemini代理系统获得，随后由人类作者核验和编辑；其他论文能够直接证明研究产物存在，但代理具体完成了多少工作，仍主要依赖项目方对工作流程的描述。

上游代码提交提供了另一类外部信号。Eigen的单行或单列矩阵向量运算优化，以及ParlayHash相关改动，已经进入公开项目并经过维护者的代码审查；这能确认改动真实存在并获上游接受，但不能单独证明项目方公布的全部性能数字可在不同软硬件条件下重现。

Teamwork会在运行中改变代理数量和结构

Teamwork不是让固定数量的代理沿预设流水线依次作答。框架将编排逻辑与代理角色描述分开，可按任务选择Iterative Coding、Distributed Coding、Long Proof、Self-Verification或Document Review等模式，并在运行中决定需要多少代理、多少轮协作以及何种团队结构。

用于开放数学问题的Long Proof模式把大量计算放在策略筛选阶段。多个代理并行提出候选路线，每条路线配有专门寻找反例或漏洞的“否证者”；综合环节比较候选方案及批评意见，被推翻的路线仍会保留可用想法和已发现的问题。

通过筛选的策略会被拆成具有明确依赖关系的子问题。相互独立的部分可以并行处理，有前置关系的部分按依赖顺序推进；每个子问题内部还会经历生成、批评、综合和重试。这样的动态组队扩大了搜索范围，也意味着研究运行的计算开销和并行度可能高于公开预览配置。

71%和0.71%仍需与公开产物分开看

TCSBench是Google内部开发的理论计算机科学评测集。71%对应Gemini 3.7 Flash、Gemini 3.1 Pro和Long Proof共同构成的配置，高于较早配置的67.7%，但它不是3.7 Flash单模型成绩，也不是外部排行榜或独立实验室的复测结果。

处理器模拟实验的边界相似。Teamwork使用Gemini 3.7 Flash从头构建了周期级、乱序执行的RISC-V模拟器，使其能够把xv6启动到命令行并运行超过100项标准基准；在未见测试负载上，项目方得到相对BOOM硬件执行基准0.71%的平均周期对齐误差。

该实验将Spike参考模拟器的源代码与代理隔离，并通过锁步协同模拟比较执行结果，以减少直接读取参考实现的可能。模拟器代码和xv6启动状态属于可以观察的产物，0.71%则是特定实验安排下的测量值；两者不能使用同一层级的“已验证”标签。

目前可以确认产物存在，不能外推通用科研能力

现有公开材料支持一个较窄的结论：Gemini模型与Antigravity Teamwork的组合产出了一批可供外部检查的论文、Lean证明和上游代码，并展示了运行时调整代理规模及分工的长周期协作机制。不同成果能接受的外部检查方式并不相同。

更强的结论尚未成立。七项工作的类型、模型配置和验证方法并不统一，部分结果属于复现或依赖假设的结论；内部基准及处理器对齐数据也不能直接证明系统已获得可迁移到任意学科的通用科研能力。

证据边界因此应停在已经公开的具体产物：形式证明可以交给Lean检查，论文可以审阅，代码提交可以复查；内部百分比只能作为项目方在特定配置下取得的测试记录。只有出现同行评议决定、独立复跑数据或公开配置下的重复结果后，相关结论才可能进一步扩大。