这两天你的信息流里大概率刷到过两条新闻，先别急着转发。
第一条：Claude用11天"验完"了费马大定理。Anthropic刚刚官宣，1300万行代码、60亿token，这条是真的。36氪
第二条：豆包"证明"了黎曼猜想。有网友说自己引导豆包完成了完整证明，知乎相关问题下最热的一条回答浏览了近500万，但数学圈没有一个人认账。知乎同一周，同样的"世纪难题"关键词，一条是里程碑，一条是段子。今天把这本账摊开：哪些AI数学新闻是真的、哪些是假的，以及你以后怎么自己一眼分辨。
先把传得最广的那条纠正掉：Claude没有"证明"费马大定理
费马大定理1995年就被怀尔斯证完了，这是30年前的旧账。Claude这次做的事情叫形式化——把人类已有的证明翻译成机器能逐行核验的Lean代码。B站、小红书上满屏的"Claude证明费马大定理"，标题全部失真，知乎已经有人专门写文章纠偏。
那这件事牛在哪？看数字：约11天，1300万行Lean代码，沿途证明30300条定理，最终链路用了其中29500条，烧掉约60亿输出token。作为对照，业界原本预估这是个多年工程——2024年帝国理工的Kevin Buzzard教授刚启动一个专门形式化费马大定理的社区项目，光第一阶段的蓝图就写了86页。
干活的是数十个Claude agent组成的流水线：Prove2Me工具把全部任务组织成一张定理依赖图，agent们并行推进、共享状态，失败的分支也会留下可复用的代码。给这套系统掌舵的是清华姚班出身的彭天翼——他不逐行写代码，只在关键处给高层指示，比如优先处理某个数学对象。
机器核验和"很多专家读过了"是两种硬度。Lean不接受"显然可得"，每一步推导都要从公理写死。这次有两道检查：第一道查推导，最终证明只用了Lean的三条标准公理，没有为费马大定理偷偷加专用假设；第二道查目标，比对器确认最终证明的定理陈述和Mathlib库里的费马大定理完全一致——防止几十个agent干了11天，中途把题目悄悄换成一道简单版。知乎那张依赖图上，Mazur、Ribet、Wiles三条主线一路汇聚到费马大定理的终点节点，每个节点都是一条机器验收过的定理。
还有两个细节值得记住。一是Anthropic自己承认，这1300万行代码规模是整个Mathlib数学库的5倍，“很可能远长于必要长度”——它是工程奇观，不是优雅证明，129页论文给人看思路，1300万行代码给机器查对错，两者不互相替代。二是一个更亲民的对照实验：三个个人版Claude Max订阅（消费级，按月付费那种）协作3天，完成了Vinogradov三素数定理的形式化。这条"验证流水线"已经下放到普通人订得起的档位。
真账：2026年至今，这几条可以放心转
把今年AI数学的真成果按时间捋一遍，每条都带验证方式：
1. 2-3月，Claude Opus 4.6解决Knuth正在研究的图论问题。 高德纳（《计算机程序设计艺术》作者）研究有向哈密顿回路的分解问题，被Claude接过去了。
2. 5月21日，OpenAI未发布模型推翻Erdős单位距离猜想。 1946年提出的80年猜想，模型构造出一个新点集，单位距离数量直接超过猜想允许的增长范围。微博这条是"证伪"，比"证明"更炸——猜想本身错了。
3. 7月，GPT-5.6 Sol几天内连下6个Erdős问题（#390、#486、#536、#788、#1002、#1038），部分成果已做Lean形式化。
4. 7月21日，Claude Fable 5与Anthropic数学家Levent Alpöge合作找到雅可比猜想的反例。 Keller 1939年提出的猜想，立了87年，在三元多项式映射场景下被证伪。
5. 8月1日，OpenAI内部模型Astra一次性公布10项数学与理论计算机成果，全部做了Lean形式化。这批结果的token消耗按API价格折算，约2000美元。
6. 8月，协和医生+GPT-5.6 Sol证明克鲁泽猜想，这条单独讲，见下文。
7. 8月11日前后，Claude冲击黎曼猜想本体。 Anthropic内部有人给一个未发布的研究版本布置了这道"不讲道理"的任务。它先提出650个思路，全部失败；随后组织约60个子Agent连续工作一天半，执行2400次Shell命令、写下数百个Python脚本。36氪黎曼猜想没被证明，但"临界线上零点占比"的下界从约41.6%推到了67.2%。这个幅度什么概念？此前37年，人类总共只把这个比例提升了0.8个百分点。微博Menlo Ventures合伙人Deedy的评价是：这可能是2013年有界素数间隔突破以来，解析数论最重大的进展。而且这条结果自带证书：Claude给出了对应的Lean形式化证明，Anthropic两名数学家完成验证，数论学家Brian Conrey和Dan Goldston也审阅了论文。
克鲁泽猜想的故事最有小说感。主角金山木是北京协和医院神经外科住院医师，本科读的是地质，数学全靠自学，起因是研究经颅超声时接触到矩阵分析。他把OpenAI之前解另一个猜想用的提示语改写后交给GPT-5.6 Sol，设定模型不联网、不读文件，让它自己探索多条证明路线、自己反复查漏，模型一口气跑了16个小时，他中途没有干预。之后，康奈尔副教授汤森德、华盛顿大学荣休教授格林鲍姆、克鲁泽本人从头核验了证明。8月20日，克鲁泽在给中国新闻周刊的回信里说，他很满意，自己的猜想已经成为定理。中国新闻周刊汤森德还补过一个背景——他常年让ChatGPT试证这个猜想，模型经常给出"看似完整、一查就错"的论证，这次的含金量在于核验真的过了。
再说这几天刷屏的GPT-6把孪生素数方向的有界素数间隔上界从246推到186。这条线的谱系是：2013年张益唐的7000万 → Maynard压到600 → 陶哲轩带队收窄到246 → 之后停滞10年以上。微博这次的证书来得很快：OpenAI研究员苏炜杰（宾夕法尼亚大学统计学教授、北大数院07级校友）在X上宣布进展并确认完成了Lean形式化验证，OpenAI同步挂出论文《Improved Short Gaps Between Primes》，摘要里直接写明：该数学证明由GPT-6 Astra给出。36氪
9月4日还有一条容易被忽略的：广东工业大学、华南师大、上海交大、杜克大学联合团队发布Eureka架构，在黎曼猜想的另一条证明路线（局部Weil二次型正性）上，把关键边界推进到理论第一道门槛的99.55%。36氪它的思路很特别：不给AI一个固定的"大脑"，而是让它在解题过程中按需"生长"出带专属记忆、工具箱和验证标准的专用宏代理。真账里不只有OpenAI和Anthropic。
假账：两条已翻车，一条蹲一手
豆包"证明"黎曼猜想：段子。 那个知乎问题下浏览最高的回答没有任何正经分析，是一张梗图。严肃回答是这么说的：AI是啥离谱结论都敢往外说，主打一个赛博生命没有脸皮。知乎补一个硬事实：黎曼猜想前10万亿个零点早就被计算机逐个验证过了，靠"穷举零点"永远证不完它；而这个所谓完整证明，没有Lean证书、没有预印本、没有任何一位数学家认账。三样全空。
Grok-3证明黎曼猜想：2024年11月的旧谣。 早被标记为虚假案例，这周又被翻出来混着新热度传播，看到直接跳过。
Claude解纳维-斯托克斯方程：蹲一手。 9月5日网传，没公布过程、没形式化、没专家签字。知乎上最诚实的回答就四个字：先蹲一手。知乎我也蹲。
三条假消息有个共同点：证据只有"模型自己说证出来了"的聊天截图。
真正的分水岭：不是算力，是证书
真假放一起看，规律非常清楚——AI数学新闻的可信度，几乎完全取决于一件东西：有没有可复核的证书。Claude的费马大定理有1300万行Lean，今天就能重跑核验；黎曼零点67.2%有Lean形式化证明，Anthropic两名数学家完成验证、数论学家Conrey和Goldston审阅；孪生素数186有OpenAI论文加Lean形式化；克鲁泽猜想有三位实名数学家签字；豆包的黎曼猜想只有截图。
Eureka的测试结果同样是拿"证书"说话的：170项复杂长周期任务，系统生成了3948份可验证的合格证书，全程没有出现一次虚假的"任务完成"报告。36氪AI可以批量生产"机器能查的证明"，但"查"这道工序反而更金贵了。
数学恰好是AI最能"干净自证"的领域，因为它有不需要信任任何人的验证器。这也是为什么这一轮真假能当场分开——换到AI写诗、AI画画，你根本没有这种一锤定音的手段。
而真正的大新闻藏在成本账里：
形式化费马大定理：业界预估数年 → 实际11天
Astra的10项成果：token账单约2000美元
克鲁泽猜想：16小时
三素数定理：3个消费级订阅、3天
验证曾经是数学界最贵的环节，现在价格正在坍塌。陶哲轩的判断很到位：数学正在从"证明稀缺"时代进入"证明过剩"时代，瓶颈不再是谁能证出来，而是谁能把证出来的东西读完、消化掉。知乎微博上有位用户一句话点破：现在问题是证明看不过来。微博
下次转发前，就问三个问题
证书在哪？ Lean形式化、预印本链接、机器核验记录，有其一才算真新闻；只有聊天截图的，按段子处理。
谁签的字？ 有没有实名数学家或机构独立核验。官方宣布和专家认账之间，还隔着一道同行评议。
原话到底说到哪一档？ AI做数学有四个档位，从低到高：形式化核验（翻译人类证明给机器查）→ 推进已知边界（把纪录挪一格）→ 找反例（证伪猜想）→ 全新完整证明。标题党最爱跳档，“验完"写成"证明”，“挪边界"写成"攻克”。
接下来值得盯的几个信号：纳维-斯托克斯传闻会不会拿出形式化或专家核验；豆包官方会不会回应这波"被证明"；克鲁泽猜想论文的正式发表进度；以及黎曼猜想本体——Claude那套方法Anthropic自己都说了"预计无法直接导向最终证明"，谁先真正碰线，才是下一个大新闻。
下次再有人在群里丢一句"AI证明了黎曼猜想"，你知道该怎么回了：先让他把证书发过来。
而本周真新闻其实比假新闻硬核得多——AI没有变成数学家，它变成了数学的质检员，而且质检费从"数年"跌到了"11天"。这句话，才是值得转发的那条。
