ai-powered-markdown-translator使用 gpt-5.4-mini 从法语翻译成中文的文章。
本周，Google DeepMind 在数学研究上借助 AlphaProof Nexus 实现了一个重要突破，这个代理能够解决几十年来一直悬而未决的问题。Anthropic 方面，Claude Code 的 auto mode 向 Pro 计划开放，并集成了 Sonnet 4.6。GitHub 将 Eclipse 的 Copilot 插件开源，Alibaba 则为 Qwen3.7-Max 启用了隐式缓存。
AlphaProof Nexus — 一个 AI 代理解决了几十年来悬而未决的数学问题
2026 年 5 月 25 日 — Google DeepMind 宣布推出 AlphaProof Nexus，这是一个由 Gemini 驱动的形式化证明研究代理框架（agentic framework），并于 5 月 21 日提交了一篇 arXiv 论文（arXiv:2605.22763）。
该代理基于一个循环：通过 Gemini 生成，再通过 Lean 证明语言进行形式化验证。这个组合确保了所生成证明的数学严谨性：LLM 提出方案，Lean 进行验证或拒绝，代理再继续迭代。
已发布结果：
| 领域 | 结果 | 背景 |
|---|---|---|
| Erdős 开放问题 | 353 个评估中解决了 9 个 | 其中 2 个已开放 56 年 |
| OEIS 猜想 | 492 个中解决了 44 个 | 在线整数数列百科全书 |
| 代数几何 | 解决了 1 个开放问题 | 已开放 15 年 |
| Min-max 优化 | 解决了 1 个开放问题 | 已开放 7 年 |
每个已解决问题的成本仅为几百美元——这个量级说明，代理式方法在形式化数学研究中的经济效率相当可观。
AlphaProof Nexus 已经与多个领域的数学家合作部署：组合数学、图论、代数几何和量子光学。该工作延续了 AlphaProof（2024）的方向，后者聚焦于奥林匹克竞赛级别的问题。AlphaProof Nexus 则瞄准 研究型开放问题，标志着 AI 作为自主数学发现工具向前迈出了一步。
“AI agents are advancing research-level math.”
🇨🇳 AI 代理正在推动研究层面的数学进展。 — Pushmeet Kohli，Google DeepMind 研究副总裁，在 X 上
Claude Code v2.1.149 — 按类别 /usage 细分并修复 25+ 个问题
2026 年 5 月 23 日 — Claude Code 2.1.149 版本已发布，实现了 Boris Cherny 上周宣布的按类别 /usage breakdown 功能。
| 功能 | 细节 |
|---|---|
/usage breakdown | 按类别的消耗细分：skills、子代理、插件、MCP 服务器 |
/diff navigation | 键盘导航：方向键、j/k、PgUp/PgDn、Home/End |
| GFM task lists | Markdown 复选框（[ ] / [x]）显示正常 |
| Enterprise | 新的受管参数 allowAllClaudeAIMcps，用于 managed-mcp.json |
该版本还修复了二十多个 bug：PowerShell 中绕过 cd 权限、macOS 上与 find 相关的 vnode 表耗尽、managed-settings 对话框卡死、/config 中的幽灵改动、/insights 在缺少可选字段时崩溃，以及工具调用之间反映式 spinner 始终保持琥珀色等问题。
同日发布的 2.1.150 版本只带来了内部基础设施改进，没有可见变化。
Claude Code Auto Mode — 在 Pro 上可用，集成 Sonnet 4.6
2026 年 5 月 23 日 — Anthropic 宣布 Claude Code 的 auto mode 有两项扩展：
“Two updates to auto mode: · Now available on the Pro plan · Sonnet 4.6 is now supported, alongside Opus 4.7. Shift+tab, and let Claude run.”
🇨🇳 auto mode 迎来两项更新：现已可在 Pro 计划中使用；并支持 Sonnet 4.6，与 Opus 4.7 并列。按下 Shift+tab，让 Claude 自己工作。 — @ClaudeDevs 在 X 上
auto mode 通过 Shift+Tab 启用，使 Claude 能够在无需每一步都人工确认的情况下自主执行操作。此前它仅向更高级别计划开放，现在已经面向 Pro 订阅用户开放。新增的 Sonnet 4.6 为长会话提供了比 Opus 4.7 更经济的选择，可减少自主模式下的信用额度消耗。
要访问这些变更：claude update 或更新 Claude 桌面应用。该公告在 X 上获得了 118 万次浏览。
GitHub Copilot for Eclipse — 在 MIT 许可证下开源
2026 年 5 月 21 日 — GitHub 已将 GitHub Copilot for Eclipse 插件开源，可在 GitHub 上以 MIT 许可证获取，地址为 github.com/microsoft/copilot-for-eclipse。
整套功能都已开放，便于社区贡献：
| 功能 | 状态 |
|---|---|
| Code completion（行内补全） | 开源 |
| Next Edit Suggestions (NES) | 开源 |
| Chat（对话流、工具调用） | 开源 |
| Agent mode（多步骤代理式工作流） | 开源 |
| Skills 和 prompt files | 开源 |
| BYOK (Bring Your Own Key) | 开源 |
| 自定义代理、子代理、agent plan、MCP | 开源 |
其动机是透明性，以及在 Eclipse 开放生态精神下推动社区创新。自开放以来，社区已经提交了贡献。
Qwen3.7-Max — 生产环境已启用隐式缓存
2026 年 5 月 25 日 — Alibaba 在其面向代理的旗舰模型 Qwen3.7-Max 上启用了隐式缓存（implicit caching）。
该缓存会自动应用于所有 API 请求——无需修改代码。开发者可立即在重复上下文中获得更快、成本更低的请求。对于更高且可确定的缓存命中率，Alibaba 建议使用显式缓存，其文档可在 Alibaba Cloud 上查看。
简讯
-
MiniMax Hailuo AI 亮相香港 AIFF（HKUST） — 香港科技大学举办的第二届 AI Film Festival 收到了来自 80 个国家的 1300 份投稿。Hailuo AI 与 Tencent 和 Z.ai 一同出现在关于 AI 电影民主化的圆桌讨论中。 🔗 minimax.io
-
NVIDIA DGX Spark — 16 个本地 AI 代理同时运行 — @NVIDIAAI 转发的社区演示：2x DGX Spark（GB10）+ MiniMax M2.7 NVFP4 可同时流式运行 16 个 AI 代理，且无需云端 API。 🔗 @NVIDIAAI 在 X 上
这意味着什么
形式化数学研究的一个转折点。 AlphaProof Nexus 标志着一次突破：AI 不再局限于竞赛题或学术基准，而是开始挑战数学家几十年来未能解决的开放问题。Gemini + Lean 的组合创建了一个形式化验证循环，确保证明不仅“看起来合理”，而且是真正确的。每个问题仅需几百美元的成本表明，这种方法正变得足以被研究实验室采用，而不只是大型科技公司专属。
Anthropic 侧代理工具链的成熟。 auto mode 登陆 Pro 计划并集成 Sonnet 4.6，表明 Anthropic 认为自主代理式使用已经足够稳定，能够面向大众。2.1.149 版本加入按类别 /usage breakdown，则回应了构建复杂多代理系统的开发者的一个现实需求：准确了解哪些部分在消耗配额，以便优化架构。
开放性 vs. 软件主权。 在 MIT 许可证下开源 Eclipse 版 Copilot，以及在 Qwen3.7-Max 上启用隐式缓存，体现了两种争夺开发者的不同策略。GitHub 依靠透明性和 Eclipse 生态来扩大 Copilot 在企业 Java 环境中的采用。Alibaba 则通过无摩擦地自动降低成本，让 Qwen3.7-Max 在与云端替代方案的竞争中更具优势。
生成式媒体的工业化正在推进。 MiniMax 参加香港 AIFF——1300 份投稿来自 80 个国家——以及 NVIDIA 在 DGX Spark 上进行的 16 个本地代理同时运行演示，共同描绘出一个生态：AI 视频创作正在进入电影制作的专业工作流，无论是在电影节现场，还是在本地基础设施中。