Anthropic 用 Claude 自动验证现有代码并生成数学证明
Anthropic 使用 Claude 为现有软件生成数学证明，并由独立验证程序 Rocq 自动检查；Anthropic 称，Claude 在数周内生成约 1.8 亿行证明代码。验证条件限于特定处理器架构、单线程程序和小于 64 MB 的输入，单项证明可能消耗数亿个 tokens。
#推理
The Decoder精选AI 评分7676 The DecoderAI 评分7474 Moonshot AI 发布 Kimi K3.1 Pro，Artificial Analysis Intelligence Index 排名第四
Moonshot AI 发布推理模型 Kimi K3.1 Pro；该模型在 Artificial Analysis Intelligence Index 得分为 55，较 Kimi K3 提高 11 分，排名第四。
TechCrunch · AIAI 评分7575 OpenAI Decisions API 向所有客户开放
OpenAI 已将 Decisions API 向所有客户开放；该 API 于 9 月 29 日的开发者日宣布。OpenAI 将 ChatGPT Luna 重新配置以提升推理速度、降低成本，并为公开版本加入语音和视觉模态；OpenAI 称，速度从 1 至 3 秒缩短至 100、120 或 180 毫秒。
TechCrunch · AIAI 评分6464 MIT 研究人员让 13 个 AI 智能体在虚拟岛屿自主探索并自发玩耍
MIT 研究人员让 13 个分别运行 Claude Opus 4.7 的 Eko 智能体在模拟荒岛上无特定任务地探索 30 小时，研究者认为它们表现出类似玩耍的行为。之后，这些智能体在特定挑战中的表现通常优于未参与岛屿探索的相同智能体；其中 6 个还学会了研究者未预设的投掷技巧。研究结果发表于 arXiv，伯克利认知科学家 Eunice Yiu 表示，判断这些行为是否确实体现认知还需要更多证据。
Latent Space精选AI 评分8383 Latent Space 汇总 Kimi K3.1 Pro 发布、独立评测与权重开放进展
Latent Space 汇总了 Kimi K3.1 Pro 的发布信息与社区反应：Moonshot 称该多模态 MoE 模型有 2.8T 总参数、104B 激活参数和 1-million-token 上下文窗口，并提供 Standard 与 Highspeed 版本。
推荐理由：这篇综述把独立评测、厂商宣称与用户反应分开呈现，并对比模型能力、任务成本和权重发布状态，提供了理解发布争议的多重依据。
Simon WillisonAI 评分8080 Kimi K3.1 Pro 登陆 Kimi API，Moonshot 承诺 11 月 4 日前发布权重
Kimi K3.1 Pro 于 10 月 23 日登陆 Kimi API，Moonshot 承诺在 2026 年 11 月 4 日前发布完整模型权重。标准版输入价格为每百万 tokens $2.00、输出价格为每百万 tokens $10；另有速度快 2-3 倍的 Highspeed 版本，价格为两倍，但输入 token 缓存命中价格不变。
AWS Machine Learning Blog精选AI 评分7676 Amazon SageMaker AI 多轮强化学习实战指南：训练 gpt-oss-20b 玩 Wordle
AWS 介绍如何在 Amazon SageMaker AI 上用多轮强化学习（MTRL）训练智能体完成需要连续决策的任务，并以 Wordle 演示从部署 AgentCore 智能体、准备数据到训练和评估的完整流程。
推荐理由：文章把多轮强化学习从任务设计、奖励函数到训练评估串成可复现流程，并展示服务设置会显著影响 Wordle 验证结果。
Latent SpaceAI 评分4848 AI 正变得擅长数学：原因何在
OpenAI 和 Anthropic 的模型近期解决了多个开放数学问题，促使作者探讨 LLM 为何能处理这类难题，以及哪些问题更容易被解决。文章认为，人类通常先广泛探索、再深入少数方向，而模型可借助并行尝试和自动验证器快速筛选完整论证，从而改变搜索方式。
Microsoft Research精选AI 评分8585 Microsoft Research 研究者与合作者证明 KLS 猜想，解决 31 年数学难题
Microsoft Research 研究者与合作者证明了提出于 1995 年的 Kannan–Lovász–Simonovits（KLS）猜想，证明相关界限不随维度增长。研究团队采用人类引导的 AI 智能体搜索流程，探索了约 100 条研究路径；同等总 token 预算下的无引导尝试未能解决问题。独立团队随后给出并行证明，另有 Lean 4 形式化验证工作。
推荐理由：研究展示了人类引导 AI 智能体探索数学思路的具体流程，并与同等 token 预算下未能解决问题的无引导尝试作了比较。