11 天验完费马大定理，99.9% 却被榜单拆成两套口径

Anthropic 交出费马大定理的首个机器可检验证明

9 月 4 日，Anthropic 在官网放出《Formalizing Fermat’s Last Theorem》：Claude 用 11 天写出了费马大定理第一个端到端、由计算机逐行检查过的证明，沿途写下约 1300 万行 Lean 代码，产生 30,300 个可机器验证的定理，最终证明用掉其中 29,500 个。成品规模超过它赖以构建的 Mathlib 五倍以上。

项目由 Anthropic 研究员、哥伦比亚大学形式化工具组负责人 Tianyi Peng 发起，走的是 Darmon、Diamond、Taylor 对怀尔斯证明的简化版本。人类给出的数学输入被压缩到偶尔几句高层指令，Anthropic 公开的两句原文是「Jacobian as a scheme sounds high priority」和「push the Mazur theorem to be done soon」。算力侧消耗约 60 亿输出 token，来自一个与 Claude Fable 5.1 大致相当的内部研究模型。

转折发生在工程侧而非模型侧。早期一批 agent 各自为战，很快丢失项目状态、停止协作，那些失败的尝试最终占了成品非样板代码行的约 7%。换成 Prove2Me 之后才跑通：平台维护一张定理陈述的有向无环图，agent 只挑依赖已经变绿的节点下手；定理陈述与证明分文件存放，Lean 重编译量随之下降；每条陈述附带自然语言描述，agent 可以检索复用而不必重复证明。

验证标准堆得比一般数学论文高。成品只依赖 Lean 的三条标准公理（propext、Classical.choice、Quot.sound），经 Lean 内核检查，再由 comparator 确认定理陈述与 Mathlib 里的 FLT 表述一致。Anthropic 另做了一个对照实验：三个个人版 Claude Max 套餐的 agent 经 Prove2Me 协作，用三天形式化了维诺格拉多夫三素数定理。

编者评： 这条成果的诚实之处在于 Anthropic 自己划清了边界——没有发现新数学，novelty 落在「验证」二字上。值得抄进笔记的是那个 7%：失败的分支没被丢弃，算进了最终证明的非样板代码行。把走不通的尝试当库存而不是垃圾，是这轮 agent 工程里最实用的一条经验。

AI Bacon：Buzzard 说它「数学上什么都没告诉我们」

9 月 5 日凌晨 1 点 11 分（UTC），AI Bacon 发出一篇拆解长文，把上面那份证明的仓库扒了一遍。仓库数据比官博更精确：60,475 个模块、29,511 条定理、1,450 个定义，基于 Lean 4.33.1 与 Mathlib v4.33.0，Apache 2.0 授权。文章逐项列出「没有的东西」——无 axiom、无 sorry、无 native_decide、无 unsafe、无 partial def、无 #eval。Lean 内核像逐箱开验的海关官员，sorry 相当于贴一张「信我，没问题」的便签，这里一张都没有。

独立复核做了三层：comparator 比对挑战陈述，nanoda 0.4.13（一个用 Rust 写的独立 Lean 内核）跑过 1,052,234 条声明零报错，Buzzard 本人又编译了一遍。作者给了一句公允评价：三道独立检查，比多数已发表数学得到的待遇还高。

带刺的部分在后半段。Buzzard 当天发帖，标题是「Anthropic has beaten me to it」，紧接着泼冷水：这份工作在数学上「tells us essentially nothing」——他早就说过，自己对 FLT 证明正确性的把握是 99.9%。他主持的帝国理工 FLT 项目拿的是 EPSRC 的 EP/Y022904/1 资助，跑到 2029 年 9 月，数学策略由 Richard Taylor 定。AI Bacon 同意这个判断，却给出另一层读法：这仍是本周最有意思的 AI 结果，理由不在模型，在调度器——Prove2Me 本质上是个构建系统，定理是目标，依赖是前置条件，谁都不会互相阻塞。

编者评： 「证明了我们早就知道的东西」听着像贬损，换个角度却是这类工作最理想的形态：结论无争议，过程可审计，工程可复用。数学界拿它当里程碑意义有限，做 agent 流水线的人应该把它当参考实现读一遍。

ARC Prize 把 99.9% 拆成两套口径，贵的那套反而分数更低

官方通稿里 ARC-AGI-3 的 99.9% 这两天被反复引用。ARC Prize 的榜单页面给出了完整对照，同一批模型在两套评测脚手架下跑出的数字摆在一起：GPT-6 Astra 在 High 推理档下，Provider Adapter 口径 99.9%、花费 1.88 万美元；Standard 口径 54.8%、花费 4.07 万美元。Standard 的最高分出现在 Max 档，62.7%、2.61 万美元。

落差最大的一档是 Low：Standard 17.5%，Provider Adapter 98.0%。Provider Adapter 在所有推理档都落在 96.7% 到 99.9% 之间，Standard 则从 Max 的 62.7% 一路掉到 Low 的 17.5%。上一代 GPT-5.6 Sol 只有 Standard 成绩，从 Low 的 0.3% 爬到 Max 的 7.8%。

两套脚手架的区别写在页面说明里：Standard 在交互环境中沿用模型自己选定的笔记；Provider Adapter 保留推理状态并压缩较长的对话，让模型能复用先前的推理工作。费用那一列还指向一件反直觉的事——Provider Adapter 每一档都比同档 Standard 便宜，High 档差出一倍多。

编者评： 99.9% 与 54.8% 出自同一个模型、同一个推理档，差的只有脚手架。更有信息量的是价格列：分数高的那套跑得更省。拿 ARC-AGI-3 论证通用智能之前，先说清用的是哪套口径，否则两个数字谁也说服不了谁。

Matthew Berman：提前拿到 Astra 的这两天

Matthew Berman 在 9 月 4 日晚 7 点 03 分（UTC）发出《I’ve had early access to Astra… it’s INSANE》，一小时前的 6 点 04 分还有一支《3 Things to Try With GPT-6 Astra》。从 9 月 3 日下午起，他一连发了六支 Astra 相关视频，是这批创作者里节奏最密的一个。

前几支属于典型的首发反应：《GPT-6 IS HERE!!! (ASTRA)》《ASTRA IS HERE (GPT-6 RELEASED)》。等到 4 日这两支，内容从「发布了什么」转向「拿到手之后能做什么」，标题里的 early access 直接点明他属于先拿到权限的那批人。Astra 在 9 月 3 日只向 Daybreak 计划内的机构开放，9 月 4 日晚开始向 ChatGPT Plus 分批推送，Pro、Business、Enterprise 同步放行，Codex 负责人 Tibo Sottiaux 公布的规则是等待一天补一次额度重置。

编者评： 演示类视频的看点在边界而非上限。Berman 这批视频的时间戳价值在于，把「发布日」与「普通用户拿到手」之间的两天空白填上了——那两天里出现的评价全部来自有权限的人，样本本身就有偏。

TBPN：Astra 全面放行这天，节目过半在聊戴森球

9 月 5 日凌晨 2 点 04 分（UTC）上线，全长 139 分钟。John Coogan 与 Jordi Hays 的这期直播把 Astra 反应放在开场 49 秒，随后一路滑向别处：21 分 43 秒进就业报告，41 分 20 秒是「The Dyson Debate」，51 分 17 秒才轮到 Cybercab 落地，58 分起转入对 StepStone Group venture 与成长股权联席主管 Hunter Somerville 的长访谈。嘉宾名单里还有 Bar Winkler、Bridgit Mendler、Carina Hong 与数学家 Ken Ono。

当天还有一支 32 分钟的 Diet TBPN 剪辑版《Astra Reactions, Jobs Print, Cybercab Launch》，把主干内容压进半小时。

编者评： 一档科技直播在「AGI 时代」的第二天只给 Astra 留了开场几十秒，这本身就是个信号。发布疲劳真实存在：一周之内四家实验室全部出手，再大的模型也很难占住一整集节目的注意力。戴森球辩论占用二十分钟，比通稿更能说明今天 AI 话题在公共议程里的位置。

X 上的「AGI 后第一天」：我的生活一个字没变

华盛顿大学研究者 Yuchen Jin（@Yuchenj_UW）9 月 5 日发的一条帖子在社区里传开，四行排比：做不出像样的前端，幻灯片还得自己做，税还得自己报，Slack 和银行账户不敢交出去。「AGI arrived. But my life stayed the same.」她接着追问一句：如果今天的 AGI 真有那么聪明，为什么它还没法接入 Slack 替我回同事消息。

反驳来得很快。用户 corbtt 回帖说，这四条里有三条他的体验正好相反。altryne 的开场白是「your Slack??」。两条回帖把这条段子从吐槽拉回争议现场：同一批用户面对同一批工具，体验可以差到无法对齐。

编者评： 这类段子的杀伤力在于它绕开了所有跑分。「不敢把 Slack 和银行账户交出去」指向的是授权与可撤销性，不是能力上限——模型再强，也没解决出错了谁负责。能力叙事与日常可用性之间的这段距离，接下来几个月会比榜单更值得跟踪。

B 站：11 天对上数年，形式化证明被读成一场工业化

UP 主「分析学爱好者」9 月 5 日 13 点 20 分投稿《Claude形式化费马大定理证明：数学工业化》，片长 7 分 39 秒，到当天傍晚播放量已过 6.8 万，是中文区这波形式化讨论里跑得最快的一支。标题里的「数学工业化」点出了它的角度：把 11 天与社区工程原定的数年周期并排，焦点放在生产组织方式的变化上。

同一时段 B 站上还有几支同源视频：《AI 11 天完成费马大定理形式化证明！》（高等数学真高等，9 分 57 秒）、《357 年悬案 11 天验证完》（AI技术投降派）、《刚刚，Claude首次形式化证明费马大定理！清华姚班大神出手了》（晚风居住的街道Echo）。角度从科普梳理到人物叙事都有，密度差别不小。

编者评： 中文区这批视频几乎都从「11 天对上数年」切入，这个 framing 挑得准——它避开了「AI 会不会做数学」这类吵不出结果的命题，转而追问生产组织方式。缺的一环是 Buzzard 那句冷话：证明本身没告诉我们新东西。少了这一层，工业化叙事容易滑向效率崇拜。

编者按

今天这几条能被串成一条线：AI 产出的两种「可验证性」，正在朝相反方向走。

一头是 Anthropic 的费马大定理。11 天、1300 万行 Lean、三道独立检查器，仓库里连 sorry 都搜不到。这是目前 AI 交出的最硬的一类成果：有争议的部分被压到零，任何人下载下来就能自己编译一遍。Buzzard 说它在数学上没告诉我们新东西，这个判断反过来印证了它的性质——正因为没有新数学，全部价值才落在「可信」二字上。

另一头是 OpenAI 的 99.9%。ARC Prize 的榜单把同一个模型在同一推理档下的两个数字摆在一起：Provider Adapter 99.9% 花 1.88 万美元，Standard 54.8% 花 4.07 万美元。分数高的那套跑得更便宜，这件事本身就说明分数记在了谁的账上。Gary Marcus 追问架构透明度那天的核心疑问，这份榜单给出了部分答案，剩下的部分还锁在 OpenAI 手里。

夹在中间的是 Yuchen Jin 那条四行排比。它讲的既不是证明也不是跑分，是授权：Slack 和银行账户交不出去，跟模型多聪明关系不大，跟出错之后谁担责关系很大。B 站那批视频把「11 天对上数年」读成工业化，角度挑得不错，只是别忘了这批形式化成果之所以能被认真对待，靠的是可检查，不是快。

一条可以拿去用的判断标准：遇到「AI 做到了 X」这类宣称，先问三件事——有没有能自己验一遍的可下载物；数字出自哪套脚手架；失败了谁兜底。今天这七条里，答得上来的是 Anthropic 那份仓库，答不上来的是 99.9%。