8月2日 X AI 日报：Astra 公布十项数学结果，Gemini Robotics 2 展示全身控制

截至北京时间 8 月 2 日 10:00，本期覆盖 8 月 1 日 10:00 至 8 月 2 日 10:00 的 X 公开帖。窗口内最值得跟进的信号，不是又一个模型榜单，而是 AI 输出开始被要求同时满足三件事：能解决更难的问题，能在真实环境里执行，还要留下可复核的证据。

OpenAI 在 8 月 1 日发布的文章中，公开了十项数学与理论计算机科学的新结果，覆盖高维几何、编码理论、群论、量子复杂性、格密码和极值组合数学等方向。OpenAI 说，这些结果由内部版 Astra 找到，按 Sol API 价格估算，寻找解答所需的 token 成本约为 2,000 美元；随后由人类与模型共同整理成论文，并把每个论证形式化为 Lean certificate。1

Lean 是一种交互式定理证明器。它能检查形式化证明中的每个逻辑步骤，但它检查的是「这份形式化证明是否成立」，不自动回答「这个结果对数学领域有多重要」。OpenAI 也把论文、证明证书和推理材料公开，邀请数学界继续核验。

窗口内，AI 研究解读账号 Sensemaker 把这条消息的边界说得更准确：十项结果很重要，但还不能直接等同于十项已经被独立验证、被数学界接受的突破。2 这也是本期对 Astra 最稳妥的判断：它把「模型给出答案」推进到「模型给出可机器检查的论证」，但科学影响仍取决于外部研究者复核、理解和后续引用。

对读者来说，先看两件事就够了：第一，公开的 Lean 证书能否独立重编译；第二，相关论文是否在模型之外形成可复用的新方法。Astra 目前仍是未公开模型，不能把这次研究结果直接理解成一个今天就能调用的产品。

Google DeepMind 机器人研究员 Rohan Thakker 在北京时间 8 月 2 日 08:56 发帖称，Gemini Robotics 2 已发布，并把过去常见的取舍概括为「通用、全身控制、灵巧操作三者选一」，随后写道团队正在同时推进这三个方向。3

这条 X 帖子发表于本期窗口内，但 Google DeepMind 官方博客对应的发布时间是北京时间 7 月 31 日 00:00，所以这里报告的是 X 端的研究员补充，而不是 8 月 2 日新上线的产品。官方页面把更新拆成三层：Gemini Robotics 2 将视觉和语言转换为电机控制，覆盖全尺寸人形机器人和双臂机器人；Gemini Robotics ER 2 负责多步骤规划、进度判断和多机器人协作；On-Device 2 面向本地运行，并称新机器人形态通常只需数小时、少于 200 个示例即可适配。4

这条更新的门槛也写在官方材料里：多指灵巧操作仍然困难，VLA 和 On-Device 模型目前面向 early-access partners，ER 2 才提供公开预览入口。对机器人团队而言，真正要测的不是演示动作是否流畅，而是换一套硬件、遇到失败步骤或有人靠近时，模型能否停下、解释状态并把任务交还给人。

工程师 David Hendrickson 在窗口内的 X 帖子中，把 openPangu-2.0-Pro 的意义放在模型之外：如果一个前沿规模模型从训练到推理都围绕 Huawei Ascend 生态展开，开源竞争的变量就不只是一组权重，而是能否脱离 CUDA 形成另一套软硬件路径。5

模型卡给出的可核对信息是：openPangu-2.0-Pro 采用混合专家架构，总参数约 505B，每个 token 激活约 18B，支持 512K 上下文，训练数据约 34T tokens，并基于昇腾 NPU 训练。模型卡还提供推理框架和部署说明，但没有第三方复测来证明这些规格会在不同硬件上带来同等的速度或成本。6

因此，这条线索更适合被理解为「部署选择扩大」，而不是「某个模型已经赢了」。读者若要跟进，应先确认实际可用的推理框架、显存与网络拓扑，再比较吞吐、延迟、兼容性和授权条款。仅凭 505B 或 512K 这样的规格，不能推出生产环境的总成本。

Supabase 的官方 Evals 首帖早于本期窗口，发布时间为北京时间 8 月 1 日 04:02；窗口内，AI 开发者 Shugo Nozaki 继续围绕这套评测讨论，强调比模型排名更值得关注的是：失败是否被保存，修复后能否再次跑同一组真实任务。7

Supabase 的官方说明显示，Evals 会让 Claude Code、Codex 和 OpenCode 在真实 Supabase 环境中建表、调试 Edge Function、修复 RLS 策略等，再用确定性检查和 LLM-as-a-judge 评分；每次失败最多重试一次，另有每天刷新的回归套件。官方还披露，在它自己的测试快照中，Codex / GPT-5.6 每个场景大约读取 8 页文档，Claude Code 约 2 页；即使加载 skills，Claude Code 在不到 40% 的场景中检查了文档。8

这不是跨平台、独立实验室的总榜，数字会随着模型和工具变化。它的价值在于把「Agent 会不会用好我的产品」拆成可重复的任务：先记录失败，再改 skill、MCP 描述或文档入口，最后重新跑回归测试。对自建 Agent 的团队，这套思路比再换一个模型更容易立刻落地。

Imperial / Skema 研究者 LinXule 在北京时间 8 月 1 日 23:21 的帖子里，把当日关于 Codex 子 Agent、DeepSeek 的 Agent harness、Buzz 开源和 YC 的 QM 等讨论归纳为同一个方向：下一阶段的问题是多智能体协同和 AI-native 组织，而不只是单个模型的能力。9

这是一条个人判断，不是行业统计。但它能和前面的事实接上：Astra 用 Lean 处理可验证交付，Gemini Robotics 2 把规划、执行和安全停止拆成不同模型层，Supabase Evals 则把 Agent 放进真实环境里反复验收。共同变化是，模型输出不再是流程终点，权限、工具调用、失败恢复和证据链都成了产品的一部分。

本期最清晰的信号是：AI 竞争正在从「能不能生成」转向「能不能在约束下完成，并留下可复核结果」。Astra 的约束是 Lean 证明，Gemini Robotics 2 的约束是物理安全和硬件适配，openPangu 的约束是软硬件部署路径，Supabase Evals 的约束是真实任务和回归测试。它们不能互相证明，但放在同一个窗口里看，方向是一致的。

接下来值得跟踪三件事：Astra 的证明是否得到数学界独立复核；Gemini Robotics 2 在早期合作方之外的硬件适配和失败恢复；以及 Supabase Evals 的公开快照是否会随着模型和 harness 更新而改变。