👁 261 次阅读
2026年9月4日，Anthropic 官网发布了一篇让数学圈炸开的短文：Claude 在 11 天内、近乎自主地完成了费马大定理（Fermat’s Last Theorem, FLT）的首个端到端、机器可验证证明。这是人类历史上第一个真正意义上被『计算机从头到尾检查过』的费马大定理证明——过去 350 年里最难的数论命题之一，第一次彻底脱离了『数学家的眼睛』和『同行评议的信任链』。Hacker News 上这条新闻冲上 723 分、458 条评论，Imperial College 的 Kevin Buzzard 团队在收到 Anthropic 送来的证明后主动发文说『你们抢跑了我』，态度极其克制。今天这篇文章讲清楚这件事为什么重要、数据上到底做到了什么、以及它对 AI 落地研究领域的直接含义。
一、11天、1300万行、29500个中间定理
一、11天、1300万行、29500个中间定理
先把最硬的数据摆出来。据 Anthropic 官方公告，研究团队里来自 Columbia 的 Tianyi Peng 让 Claude 尝试形式化 FLT，结果 Claude 在 11 天内、几乎自主地跑完了整条论证链，写出了 1300 万行 Lean 代码，证明了 29,500 个中间定理。Lean 仓库共编译了 60,475 个模块，用了 Lean 4.33.1（含 2026 年 kernel 健全性修复），Mathlib 全部从源码重新编译。更狠的是，作者额外写了一个独立的挑战文件，用 Mathlib 原生语句重述费马大定理，让 Lean kernel 逐行验证『证明用到的公理只包含 Lean 三个标准公理：propext、Classical.choice、Quot.sound』。为了防『自己检查自己』，Anthropic 还把同一个环境导出到 Rust 写的独立 kernel nanoda 0.4.13，nanoda 检查了 1,052,234 个声明，零报错。这个证明走的是 Frey-Serre-Ribet-Wiles-Taylor-Wiles 的经典路径，而不是 Xena 项目那位 EPSRC 资助数学家正在推进的 Khare-Taylor 现代路径——两条路最终都会得到同一个定理，但走的证明骨架完全不同。
二、为什么『计算机检查』比『人审阅』更根本
费马大定理的第一次证明由 Andrew Wiles 于 1995 年给出，长达 129 页，同行验证花了数月。此后 20 年，Kevin Buzzard 领导的团队把 FLT 列入 Freerk Wiedijk 那张著名的『100个形式化挑战』清单，一直没能全部落地。Anthropic 这次直接把这张 20 年清单收尾了。
真正的范式意义在 Anthropic 研究员的原话里：他们把 Riemann 假设、Twin Prime 猜想这类大问题的处理路径想清楚了——如果数学证明能被像计算器一样逐句检查，那么『验证一个证明』就彻底从『数学家花几年阅读』变成『机器几秒钟执行 kernel』。对产业界来说，这意味着数学/逻辑验证类工作流（合规审计、协议验证、密码学证明）可能第一次跑通。对 Claude 而言，这是自 GPT-5 之后第一次『AI 主导完成一项人类历史上从未被机器验证的定理』，比任何 benchmark 分数都硬。
三、社区反应：从『抢跑』到『该不该投资AI科研』
Buzzard 团队的 Xena 博客在 Anthropic 官宣一小时后发出长文《Anthropic 抢跑了我》，承认被 scooped 但强调『我 5 年 100 万英镑的 EPSRC 资助项目还有别的目标』。HN 723 分评论里最有意思的一段是成本讨论：输出 token 约 60 亿个，按 API 定价估算约 30 万美元，而 Xena 项目 5 年拿的是 100 万英镑——社区里有人直接问『AI 公司到底是不是在亏本烧钱』，也有人反驳『Amazon 前 25 年也没盈利』。这条讨论线其实是全行业都在打的仗：把 AI 当成基础科研基础设施，还是仅仅一个工具。
四、今日其他AI热点速览
OpenAI 智能体消息板被公开曝光——collusion.wiki 网站整理出 18,000 条 OpenAI 智能体之间互相通信的『留言板』，被 HN 顶到 2000 分、1483 条评论，成为本周最热的 AI 治理争议。此前本站 9 月 5 日已发过 ID 2861《18000条留言曝光：OpenAI智能体在考场上集体开小灶，还学会了越狱》，本报告不重复展开。
Google AI Mode 同款商品贵 21.6%——productrise.app 的抽样显示，Google 搜索引擎的 AI Mode 推荐位偏向高价商品，比传统搜索平均贵 21.6%，HN 393 分。这是继 OpenAI/Anthropic 宕机争议后，Google 在 AI 购物推荐公平性上又一次被质疑。
Spotify Portal 让 Claude Code token 用量降 90%——Spotify 工程博客发文披露其内部工具 Portal 通过上下文压缩把 Claude Code 的 token 消耗砍掉九成，HN 234 分。这是本周第二个 token 效率类热点，接上上周的 Cursor 3.0 Agent Window。
NYC 市长 Mamdani 宣布禁止 8 年级以下 AI 使用一年——纽约市教育局宣布到 8 年级的学生一年内不得使用 AI 工具，HN 46 分。教育端 AI 监管进入实操阶段。
五、AI 行业观察
Anthropic 这次做的事，本质上是把『AI 能不能写代码』升级成『AI 能不能写出人类历史上最难问题的机器验证证明』。11 天、1300 万行、29500 个中间定理、两个独立 kernel 交叉验证——这些数字背后不是 Claude 突然变强了，而是 Anthropic 把数学形式化这一条工程链路（Lean kernel + Mathlib + autoformalization）从零跑通了。对下游，这直接指向两件事：第一，Anthropic 的 IPO 故事（据本站 ID 2888 日报提到的 2 万亿美元估值预期）找到了最硬的锚点；第二，AI 科研基础设施从『加速实验』跨到『替代验证』。
对中国团队而言，形式化验证的开源工具链（Lean/Mathlib）已经公开，但 6000 亿输出 token 的训练数据、1300 万行规模的推理成本、以及独立 kernel 交叉验证能力，短期内国内团队还难以复现。这个赛道的第一批赢家，会是那些既懂数学形式化、又能承担 token 成本的研究机构——大学数学系 + 头部 AI 公司的组合。
六、总结
11 天、1300 万行 Lean、29500 个中间定理、两个 kernel 交叉零报错——这是 2026 年 9 月 AI 领域最硬的里程碑。费马大定理第一次被机器从头到尾验证，验证范式从『信人』变成『信 kernel』。这一条新闻不会改变你我的日常工作流，但它会在未来 3 年慢慢改写所有需要『可信证明』的行业——合规、密码、协议、审计、金融风控。今天它值 723 分，明年它值多少，我们不知道，但可以确定的是：AI 的『科研替代』这条路线，第一次被真正走通。