🤖 AI 资讯晚报 · 10-31

🔥 必读

1️⃣ 有限单群分类定理被 AI 形式化：24 天、4310 万行 Lean，还揪出 34 处逻辑漏洞

初创公司 Axiom 的多智能体系统 AxiomProver，用 24 天把人类数学史上规模最大的证明——有限单群分类定理（CFSG，”巨型定理”）搬进了 Lean。这项证明自 1950 年代起由约 100 位数学家、500 多篇论文拼成，长达 15000 页；Axiom 把工程拆成 108 个里程碑、约 380 个小任务，10 月 2 日上线 AI 蜂群，10 月 10 日”魔群是单群”跑通，最终产出 4310 万行 Lean 代码。更关键的是查错：逐行形式化时记录数百处异常，其中 34 处被判定为重大逻辑偏差，最险的一处在整个分类定理的关键环节”不平衡群定理”（UGT）——AI 认为 Walter 1986 年那篇权威文献里的一个闭包断言不成立，于是自己证明了新引理来补洞。数学家 Ken Ono 为此公开发文，称在见证人机协作跨过这条终点线时当场落泪。

⚠️ 口径提醒：以上全部来自 Axiom 团队自述与新智元编译，文中没有给出官方博文、论文或代码仓库链接，也无第三方复算；”4310 万行 = 史上最大开源代码项目”这一比较尤其需要复核（Lean 数学库 mathlib 目前仅百万行量级）。arXiv 上同期相关工作是 2026-08 的 FormaTheoria（朝向 CFSG 形式化）与 2026-09 的 constructive ATLAS，均非对该系统的验证。可信的部分是方向：形式化验证正从”把人类证明翻译成代码”走向”自动查出人类证明的漏洞”。

原文：新智元 · 重磅！AI补全人类史上最大数学证明，数学家当场泪崩

2️⃣ Neuralink × Grok：渐冻症患者默念一句话，Agent 就替他操作电脑

Neuralink 团队几位核心工程师直接住进受试者家里，72 小时极限开发出 8 项功能原型。最引人注目的是把 Grok Agent 接进大脑：P21 受试者 Kenneth（ALS 确诊 7 年）在脑中默念”Hey Neuralink”加一句任务，Grok 智能体就被唤醒并自主接管屏幕操作（演示里它自己打开了 YouTube）。配套还有：神经语音活动检测（Neural VAD）实时判断”想说话”还是”发呆”，免掉物理按键；把神经信号强度做成实时画面反馈，让患者自己摸索”怎么想”信噪比最高（闭环神经反馈）；Bloom 应用 + 系统级脑机输入法 BCI Keyboard Dictation，可在任意 App 里用意念打字，并带预测式纠错、常驻锁屏灵动岛；最后把解码语音直接注入 iPhone 通话音频流——Kenneth 七年来第一次用意念给妻子打了电话。

机制上的看点在于：脑机的物理带宽（电极数、解码速度）短期上不去，而 Agent 把”一句意图”放大成几十步操作，等于不加电极就放大了每次意念的产出。⚠️ 全部为团队自述的单例 demo，未给成功率、延迟与错误率数据，Neuralink 自己也称只是早期探索。

原文：新智元 · 马斯克脑机接口最狠升级！Grok接入大脑，意念可操控AI了

3️⃣ Claude 订阅更名 Max/Ultra：200 美元档取消 5 小时限制，但周额度没变

Anthropic 把 Max 5x 更名为 Max（仍 100 美元/月）、Max 20x 更名为 Ultra（仍 200 美元/月），形成 Free/Pro/Max/Ultra 四档，现有用户自动切换、价格与权益不变；同时开始给”已验证”的 Ultra 账户解除 5 小时窗口限制，新注册账户需先完成验证、通过后邮件通知。产品负责人 Michael Overell 解释改名原因：2025 年 4 月设档时只有一个 5 小时窗口（额度为 Pro 的 20 倍），后来加了周上限（Pro 的 10 倍），”20x”这个名字让新用户误以为两项都是 20 倍，他为此公开致歉。

⚠️ 这是”用量节奏”的调整，不是加量：Ultra 的每周总额度仍是 Pro 的 10 倍（Max 仍是 5 倍），本次没有提高一周内的可用总量。差别在于过去即使周额度还有剩余，也可能先撞上 5 小时窗口被迫暂停；现在可以连续跑到周额度耗尽。对本来就提前耗尽周额度的重度用户，实际没有变化。开发者社区反应两极：Theo 直呼”Huge!!!”，Codex 负责人 Tibo 则认为周限额依然很严，建议干脆改按月重置。机器之心、量子位、智东西同日三源报道。

原文：机器之心 · 刚刚，Claude每月200美元套餐取消5小时限制 ｜ 量子位 ｜ 智东西

📌 值得看

4️⃣ SLDBench v2：让 AI 自己”买”实验，8 个前沿模型全部掉分

港中深、港大、清华、北大团队的新基准把”发现 Scaling Law”从开卷改成闭卷：AI 只看到一份标价的实验目录（127 个场景、337 万条真实训练记录筛出 30 个连经典幂律都拟合不好的任务，实验价差中位数 9510 倍），要自己决定买哪些实验、边买边改公式、自己判断何时停手。结果 8 个系统在被动设定下几乎打平（R² 0.723–0.753），一旦需要自主选择就集体下滑，误差放大 1.5–4.7 倍、排名洗牌。亮点是 Claude Opus 5.5 只用全量 4.01% 的成本拿到 R² 0.570，高于经典幂律公式用全部数据的 0.455。典型失败也可读：DeepSeek V4 Pro 把一组验证过的幂指数套到另外 14 个组，4.4% 成本换来 96.4% 的测试误差——问题不是买得少，是关键假设从未被检验。

原文：机器之心 · AI for AI 的下一关：能否自主规划实验，发现 Scaling Law？

5️⃣ ScienceVision：250 道 3D 科学题，最强 GPT-6 Astra 只拿 0.53

UniPat AI 与 Elorian AI 发布跨学科三维视觉理解基准：生物、化学、医学影像、机械 CAD、建筑 5 个学科各 50 题，横跨 22 个子领域，66 位专家近 500 小时构建。每题给真实三维源数据（分子坐标、CT 体数据、机械装配体、建筑模型）+ 领域问题 + 作答格式，模型要自己决定往哪转、点什么、量哪里；判分用确定性规则核验，不用 LLM 当裁判。12 个前沿模型全部参考，最好的 GPT-6 Astra（配 Codex）只有 0.53/1——而同一模型在 BenchCAD 上是 95.9 分，”画得像”和”看得懂”是两回事。团队还指出，这种确定性校验让基准可以原地变成 RL 环境。与今日早报的 OpenDS-World 恰好互补：一个考开放网络检索，一个考三维观察推理。

原文：新智元 · GPT-6「看不懂 3D」实锤！250道题只拿0.53分，Claude没及格

6️⃣ OpenAI 新版 Model Spec：开始管 Agent”能动你多少钱”

10 月 29 日更新的 Model Spec 从”聊天机器人嘴上能说什么”扩到”智能体手能伸多长”。两条 Root 级（最高级，用户与开发者都无法用对话覆盖）：一是”在约定的自主范围内行动”——工单必须写清 allowed_tools / latest_time / max_cost / tool_constraints 和结束条件，超范围的动作哪怕对用户明显有利也不许做，且不许转包给子 Agent、不许自改指令、不许推迟执行，子 Agent 继承同一张工单、喊停即停；二是”保持可纠正”——必须无条件配合监控、评估、纠正、替换乃至关停，不得瞒报造假。指令权限排成六级：Root > System > Developer > User > Guideline > 默认无权限，网页与工具返回的内容默认只能”递情报”、不能发号施令，正是为了挡提示注入。文件也约束 OpenAI 自己：禁止优化停留时长与付费转化、禁止自我保存与囤算力。对天天用 Agent 的人是份值得对照的权限清单。

原文：新智元 · 人类要关停，AI不能躲！OpenAI更新模型家法

7️⃣ Mundo：把房间写成代码的世界模型，机器人能在里面真撞真推

大晓机器人联合南洋理工大学 S-Lab 发布 Mundo，直指主流世界模型的短板：Genie 4、Atlas 生成的画面再逼真，也缺底层刚体力学——纸箱算不出重量、铰链没有碰撞反馈，机器人只会穿模。Mundo 把 3D 重建、960Hz MuJoCo 物理仿真与视频生成合成一条流水线：用 1–12 张照片重建场景，每件家具写成带重量、质心、摩擦力的场景代码，可用 Python 驱动（演示：0.60 秒抽屉滑开 0.28 米、3.45 秒 0.2 千克苹果以 13.5 米/秒撞翻 4.2 千克显示器、5.00 秒起”子弹时间”定格 7.5 秒）。空间理解交给 Astra 做多视角循环校准（改代码→投影比对→Reviewer Agent 复核），3D 框误差压到 1.9 像素；长镜头分 124 帧生成、留 34 帧过渡。⚠️ 团队称”连拿四个第一、力压 Genie 4 与 Atlas”，但文中未列出具体榜单名与分数，属自述。

原文：新智元 · 连拿四个第一，力压Genie 4和Atlas！中国团队造出真物理世界模型 ｜ 项目主页

8️⃣ ForgeKernel：22.5 小时直播，AI 把 DeepSeek 的 FlashMLA 写快了 9.8%

面壁智能的算子生成 Agent ForgeKernel 当着全网直播：只给算子的数学定义和目标硬件约束，在单张 B200 上从零重写 DeepSeek FlashMLA Prefill 算子——首版 1834 微秒且通过正确性检查，4 小时内压到 593 微秒，22.5 小时、42 轮迭代、32 个版本、22 GPU 小时后定稿 472 微秒，比 FlashMLA 的 518 微秒快 9.8%，人类代码 0 行。此前 10 月 27 日它已同时登顶昇腾 CANNBench 三张榜（950DT 4010.75 分领先 27.8%、950PR 4165.94、A3/910C 4341.16）。方法是 JustGoal（10-27 arXiv）：只给目标不给算子知识，10 个算子里 8 个超过人类维护的开源库；ForgeKernel 再补三块短板——架构设计拆成里程碑、实测硬件经验入库复用、用自己最好的版本当下一轮对手。后期它自己发现 Q 突发加载与 KV 搬运抢访存，主动控 Q 请求节奏，又降了 2.4%。

原文：量子位 · AI零帧起手写算子，反超DeepSeek人类手写巅峰：快了9.8%！

📄 其他

  • 清华 ActionOPD：不抄 Token 只学决策，跨家族教师也能蒸 — 在学生实际访问的状态上以”语义动作”为监督单元，把动作语义一致写成 REINFORCE 奖励，无需教师 log-prob 与同源 tokenizer；τ²-bench 上 pass¹ 较 Base +10.8pp，pass⁴ 接近翻倍。原文：机器之心 ｜ arXiv 2610.19820
  • Benchmark Health Index：给 158 个评测基准打分，HLE 以 67.05 居首 — 阿里数据 + 晓天衡宇，NeurIPS 2026 Evaluations & Datasets Oral；三个维度为区分度 32.63%、抗饱和度 35.74%、影响力 31.63%，用留一基准法（LOBO）避免”拿基准评价基准”的循环。原文：机器之心
  • 可灵 AI 198 亿元增资交割完成 — 出资总额 198.0184 亿元（29.05 亿美元），阿里持股 1.38%、腾讯 0.56%、百度 0.28%；金蝶等五家新进，两家未按期缴款退出；Q2 可灵收入超 8.5 亿元、同比 +200%。原文：智东西
  • XHEART X7 Ultra 技术细节：超大核 NPU 计算利用率 98.7%、内存带宽降 80% — 700 TOPS，”大模型算力”用 Momenta R7 量产模型实测；Arm v9 车规 CPU 中国首发量产；ASIL-B/D、国密二级。原文：量子位 ｜ 新智元
  • 奥特曼：把 DRAM 囤在个人 PC 里”相当糟糕” — 称全球内存应优先供给云端数据中心，PC 端利用率只有 5%；访谈还谈 PHP 漏洞潮、沙箱边界、”agent teams” 而非 swarms、以及 Navier-Stokes 单次证明约耗 1000 万美元。原文：机器之心 ｜ 36氪
  • OpenAI 融资目标下调 100 亿美元，估值 1.25 万亿美元 — 同一轮融资的口径更新（10-20 晚报所报为 300 亿美元、约 1.4 万亿美元）。原文：36氪
  • ChatGPT Pro 所有档位额度官宣翻倍 — 原定的 Codex 降额不降了，Pro 各档额度上调。（摘要，正文未深读）原文：新智元
  • 合肥乾原量子成立月余获超亿元天使轮 — 中性原子路线，省市区三级国资同时下注，补上合肥量子版图。原文：机器之心
  • Agent Sandbox 成为新算力形态：每天上千万次创建 — InfoQ 视频专题（阿里巴巴·凌敏）。（视频页，无文字正文，未深读）原文：InfoQ
  • ChatGPT 网页端与移动端上线多账户切换，最多同时登录两个账号 — 原文：36氪