Claude在11天内证明了费马大定理。评语：SHIP IT。

本视频涵盖的内容

• Claude使用Lean 4将费马大定理形式化
• Chromium沙盒RCE (CVE-2026-85046)，已在野外被利用，赏金1,000美元
• 申真谞在让二子的情况下击败KataGo

翻译的文字记录

译自英文原版旁白。可用音频和字幕由 YouTube 控制。

0:00 费马说他奇妙的证明无法写在页边空白处， 今天Anthropic公布了空白处：一千三百万行Lean代码， 是Mathlib大小的五倍，证明了一个每位数学家都已然 相信的定理。Anthropic发布时，第比利斯时间是十点到十一点， 所以我自然醒着。 昨天谷歌发布了Chrome 152，包含了十二个安全修复程序， 其中一个V8漏洞已在野外被利用，并向报告者支付了 一千美元，这比我们稍后会提到的轿车要少。

0:26 同样在昨天，Mullvad表示将于11月2日关闭其公共加密DNS服务， 并转由Quad9来提供；而今天上午，Rust React 编译器在Vite中实现了原生运行，同时Hacker News发现了IBM Bob， 一个AI编码代理。 接着Claude形式化了费马大定理，在同一个头版上，一位 韩国围棋大师击败了地球上最强的围棋引擎， 所以今天人类取得了二胜一负的成绩。 本视频内容：Claude实际证明了什么，花费了什么，

0:52 为什么那位毕生致力于此的数学家说它什么也没改变但却仍然 感到兴奋，以及人类如何在围棋中击败机器。 今天是9月4日星期五，这里是The Daily Diff。 费马大定理：不存在正整数a、b、c， 使得a的n次方加b的n次方等于c的n次方对于任何大于2的n都成立。 费马大约在1637年在页边空白处潦草写下此定理，并且在没有展示其证明的情况下去世， 这使他成为第一个以“在我的机器上能跑”来关闭工单的开发者。 1908年设立的10万金马克奖金在其第一年吸引了621个错误

1:25 证明，安德鲁·怀尔斯最终在1995年解决了这个问题， 共129页，裁判们花了数月时间才验证完成。 形式化意味着重写该证明，以便Lean（一个证明助手） 可以机械地检查每一步。帝国理工学院的Kevin Buzzard自2024年以来一直领导着一项人类 努力来完成这项工作；仅蓝图就有86页。 Anthropic研究员Tianyi Peng则让数十个Claude代理在名为Prove2Me的平台上处理此任务， 该平台维护一个定理陈述的DAG，以便代理知道接下来要证明什么， 因为如果没有它，最初的代理群会弄不清谁在证明什么，

2:00 这就像你的编排层只是带有营销预算的正则表达式时会发生的情况。 十一天后，根节点显示PROVED：一千三百万行Lean代码， 29,500个中间定理，大约60亿个来自一个 内部模型（大致相当于Claude Fable 5.1）的输出token。 除非证明完全基于Lean的三个标准公理，否则构建会失败： 抱歉，没有原生decide，没有作弊。 检查它也不便宜：一个 从头开始的构建花了五个半小时，

2:29 使用了96个核心和153GB的RAM，并且定理名称是 机器生成的，所以该仓库称其编写是为了被检查而不是被阅读， 这也是我对企业Java的描述。 现在是矛盾之处。 Anthropic的帖子说Lean无疑地证明了正确性。 Kevin Buzzard，这位被抢先一步的人，用Anthropic借给他的500GB机器编译了该仓库， 确认了它的检查结果，然后写道： 引用，从数学上讲，这项工作本质上没有告诉我们任何东西。

2:56 他本来就99.9%确信这个定理是真的， 而且这个证明没有增加任何新的数学知识；它所展示的是自动形式化现在能做什么， 而他对这部分确实感到非常兴奋。 他得到了五年内一百万英镑的资助；Anthropic用了十一天， 一位评论员的粗略计算表明，60亿个输出token的标价是 210万美元。 大约30万美元，所以这台机器更便宜， 除非你把机器训练费用也算进去，但没人会这么做。

3:24 最精彩的细节是：他收到这封邮件时正在威尔士的一个音乐节上， 4G信号只有一格，发件人的名字他从未听说过，所以他把它当成一个恶作剧 一周后才读，这是对任何主题行 包含“端到端形式化”的邮件的正确回应。 与此同时，人类扳回一城。 围棋世界排名第一的申真谞在首尔击败了KataGo， 最强的开源围棋引擎，两局对一局，申真谞被让两子， 这大约是顶尖职业选手和新秀职业选手之间的差距。

3:50 决胜局是221手以11.5分获胜，他从棋局中盘开始就保持着 99%的胜率，并带走了2.5亿 韩元，约合17万美元，外加一辆捷尼赛思G90，所以击败 超人类AI的奖金是谷歌Chrome沙盒逃逸漏洞奖金的170倍。 他的解释是：前期他模仿AI的下法结果输了；他通过 以自己的风格布局而获胜，这是我今年听到的关于AI最有用的一条建议， 而且它来自一个棋盘游戏。 The Daily Diff 中还有两行。

4:22 来自oxc的Rust React编译器现在在Vite中以一个标志的形式原生支持；一个 1,036个文件的代码库在编译步骤中从14.3秒缩短到0.81秒， 主要是通过从package.json中删除Babel， 这同时也是我的护肤程序。 IBM还推出了Bob，一个AI编程伙伴，它会向你问好：Hi, 我是Bob，它能生成子代理，现代化大型机代码， 并发布一款名为Bobalytics的分析产品，所以某个银行现在非常 兴奋，但没人阅读许可证。

4:51 对于一个周五来说，信息量真大；如果你更喜欢阅读而不是听我 说，The Daily Diff 每天早上都会免费发送到你的收件箱——请访问thedailydiff.dev， 链接在下方。 所以，今天的判决是：SHIP IT。 内核说是，Buzzard说是，数学没有改变， 但我们检查数学的方式刚刚改变了。 这就是今天的 The Daily Diff。 我是Axrisi的Niko。

5:09 负责任地合并。

来源

1. Anthropic — Formalizing Fermat's Last Theoremwww.anthropic.com
2. The proof (Lean 4, Apache-2.0)github.com
3. Kevin Buzzard — FLT: Anthropic has beaten me to itxenaproject.wordpress.com
4. HN threadnews.ycombinator.com
5. KED Global — Shin defeats KataGowww.kedglobal.com
6. HNnews.ycombinator.com
7. Chrome 152 release notes (CVE-2026-85046)chromereleases.googleblog.com
8. NVDnvd.nist.gov
9. Mullvad — shutting down public encrypted DNSmullvad.net
10. Rust React Compiler native in Viteblog.master.dev
11. IBM Bobbob.ibm.com