上周你的朋友圈大概率被"AI攻克费马大定理"刷屏过。微博上一条"数学界彻底被AI撼动了！清华姚班神童带队，Claude彻底攻克了350年的终极噩梦"的帖子转了几百次，评论里有人喊"数学家可以回去刷盘子了"，也有人冷笑"又是标题党"。微博
两边其实都没说到点上。9月4日到9月8日这五天，AI圈确实密集炸出了一串数学成果，但它们完全不是一类东西——有的是真金，有的是被误读的硬工程，还有的今天刚变成一桩罗生门。把这五天的账拆开算，你以后再看到"AI证明了XX"的标题，30秒就能判断该不该转发。
第一件事：Claude"证明"费马大定理？先搞清它干的根本不是证明
先说结论：费马大定理1995年就被怀尔斯证完了，129页，人类数学早就翻篇了。Claude这次干的活叫形式化——把怀尔斯那套"人读得懂、机器验不动"的证明，逐行翻译成Lean证明助手能机械核验的代码。打个不准确的比方：这相当于把一本天书翻译成了机器人能逐字校对的语言，翻译得极其牛，但书不是它写的。
那为什么数学圈还是炸了？因为这笔账算下来太吓人：
时间账：帝国理工数学家Kevin Buzzard拿着英国研究理事会100万英镑、为期5年的资助，专门带队做这件事，社区光前期技术蓝图就写了86页，普遍预期还要好几年。Claude用了11天。Buzzard本人下载、编译、亲自验证了Anthropic的仓库，确认没有用占位符作弊，然后公开承认：被抢先了。知乎
规模账：产出约1300万行Lean代码，是Lean社区十年积累的核心库Mathlib（约200万行）的5倍以上；过程中证明了30300个中间定理，最终29500个进入证明链；消耗约60亿输出token，用的是能力接近Claude Fable 5.1的内部研究模型。
人力账：全程人类只有一位——哥伦比亚大学助理教授、Anthropic研究员彭天翼，偶尔说几句方向性的话，比如"Jacobian当作scheme处理，优先级高一点"。知乎
60亿输出token按公开API价格粗算约30万美元，但这是账面换算，不是Anthropic的实际成本。有意思的是Buzzard自己留了个话口：他倒好奇，对方花的钱是不是比自己那100万英镑还多。Anthropic还在报告里放了个更能说明趋势的小实验：只用三个普通的个人订阅账号，让节点通过Prove2Me协作，三天就完成了维诺格拉多夫三素数定理的形式化。知乎
真正让这件事从"大力出奇迹"变成"方法论突破"的，是一个失败的开头。彭天翼最初让几十个Claude Agent自由协作，很快崩盘：Agent丢失项目状态、不知道别人证了什么、疯狂重复造轮子，最后只有约7%的非样板代码被保留。知乎破局靠的是Prove2Me系统——把待证定理组织成一张有向无环图（DAG），每个节点是一个子定理，谁证完就更新图，其他Agent立刻接力。把沿时间轴推进的数学劳动，在空间上横向铺开并行，这才是"11天"的真正杠杆。知乎
所以这条的定性：工程里程碑，不是数学里程碑。知乎上数学背景答主的吐槽也值得听一句：这1300万行代码命名混乱、文档缺失，按Mathlib的入库标准基本会被全数打回——它能过机器内核，但进不了人类数学共同体的大门。知乎
第二件事：GPT-6 Astra解出5道埃尔德什难题，这个才是"新数学"，但单价4万美元
同一周，OpenAI这边的成果性质完全不同。Epoch AI和曼彻斯特大学发布了一个叫FME（FrontierMath Erdős）的基准测试：68道人类至今没解决的埃尔德什开放难题，5个顶级模型同场考试，统一规则——每题300美元算力预算、72小时时限、禁止人类辅助，专门防"选择性报喜"。
结果：
模型 | 受控条件解出 | 备注 |
|---|---|---|
GPT-6 Astra（预发布版） | 2题（#74、#126） | 全场唯一非零分 |
GPT-5.6 Sol / GPT-5.5 | 0 | — |
Claude Fable 5.1 / Fable 5 | 0 | 交了白卷 |
放开预算后，Astra累计解出5题，包括著名的Erdős–Sós树猜想（#548），还有一题直接给出反例推翻了埃尔德什本人当年的猜想（#1）。代价是总计算花费超过22万美元——平均一道题约4万美元。微博
和费马大定理那条比，这里的每一题都是人类不知道答案的开放问题，是如假包换的"发现新数学"。但两个限定词要咬住：一是3%的成功率意味着这更像一个极其昂贵的暴力搜索过程，二是这些结果大多还要走Lean形式化和同行评审的完整流程才算落袋。人类论文里的"显然"“类似可得”，是整个学术共同体共享的隐性知识，机器必须把每一个被默认的论证都补成无可辩驳的最小步骤——这条规则同样适用于Astra的每一份成果。知乎"4万美元买一个开放难题的答案"这个单价，未来大概率会成为衡量AI科研性价比的锚点。
第三件事：今天刚爆的罗生门——数学家指控OpenAI"截胡"，这条先别急着站队
9月8日，纽约大学数学家Tristan Buckmaster公开了三篇流体力学论文，外加一份四页的个人声明。知乎论文本身很硬：他和Anthropic数学家Alpöge借助AI（Claude和OpenAI工具混用，费用自己掏），在一个月内推进了光滑外力下欧拉方程、Boussinesq方程的"爆破"证明，8月22日就通过了Lean形式化验证——这是与千禧年难题Navier-Stokes方程密切相关的方向（注意：欧拉方程不含黏性，不在克雷研究所百万美元悬赏范围内，这点媒体标题十有八九会写错）。
争议在声明里。按Buckmaster的单方叙述：9月初风声走漏后，OpenAI研究人员来电，称内部模型已生成约100页证明、走得更深，提出"协调发布与署名"，并要求把在Anthropic工作的Alpöge从署名中去掉，通话中甚至出现关乎其学术生涯的措辞。知乎双方谈崩，他索性提前公开全部论文。被点名的OpenAI研究员Bubeck否认指控，称始终遵循学术规范。
截至今天，关键通话没有录音和完整记录可独立核实，OpenAI宣称的那份100页证明也没公开，陶哲轩此前还专门辟谣过"Claude已解决NS方程"的传闻。所以这条只能给到"待观察"级别——但它暴露的问题是真的：当AI把数学产出速度从"年"压到"天"，发现与抢发、署名与归属、验证与评审的旧规则全部跟不上。陶哲轩说，数学正从"证明稀缺"进入"证明过剩"时代。知乎同行评审以年计、AI产出以天计的剪刀差，迟早要撕出这样的纠纷。这可能只是第一桩。
带走三样东西
一个分辨框架。 以后看到"AI攻克XX数学难题"，先问三个问题：是新发现还是形式化（翻译旧证明）？有没有机器核验或第三方验证（sorry-free、独立编译）？成果出自论文/基准测试，还是公司自述+截图？按这三问，上周的三条新闻分别是：硬工程但被误读、真发现但单价昂贵、真争议但证据不全。
两个性价比数字。 形式化一侧：11天+约60亿token，干翻了100万英镑×5年的人类项目预期；发现一侧：22万美元÷5题≈4万美元/题的开放难题单价。这两个数字以后会被反复引用，记住它们，你就比90%的转发者更懂这周的新闻。
三个观察信号。 ①Bubeck承诺的进一步说明，以及OpenAI那份100页NS证明是否公开；②Anthropic的1300万行Lean代码会不会被Mathlib社区消化入库——这决定它是"公共知识"还是"一次性烟花"；③"消费级订阅+协作脚手架"做严肃数学的实验能否被更多人复现——如果能，它就会从个案变成玩法。
数学没有变天，但"验算"这道工序确实开始交给机器了。至于机器能不能"负责"——Buckmaster这桩罗生门，就是第一个撞上桌面的案例。
