今天有条新闻，值得所有关注 AI 做数学的人停一下。
数学家 Simon Brendle 在 arXiv 挂出预印本（2608.19068），给出了 Hopf 猜想的证明——也就是问 S²×S² 这种乘积流形上到底存不存在正截面曲率度量，微分几何里悬了几十年的经典问题。知乎有意思的是做法：主线是人类手搓的，从 Cheeger deformation 出发设计了一组极精巧的扰动，Mathematica 只负责展开那些"看上去就很崩坏"的三角函数系数、验证三阶变分的正曲率性。全程没用生成式 AI。知乎知乎上有位做微分几何的答主说，他自己也试过让 GPT 去改进 Cheeger deformation 度量，“AI 做了几个小时做不动就放弃了”。知乎
更有意思的是，几乎同一天，知乎冒出来一个问题："如何看待 OpenAI 内部模型 SAB 解决数学界公开问题 hopf 猜想？"截至我写这篇，没有任何官方声明、没有预印本，高赞回答是阴阳怪气的反讽。知乎同一天，同一个猜想，一个实锤，一个传闻。这就是这个 8 月数学圈的缩影：AI 捷报多到看不过来，但每一条的成色都不一样。我把过去 20 天的大事捋了一遍，逐条核了一遍验证状态，帮你把"该信的"和"该让子弹飞的"分开。
先把这 20 天发生了什么列出来
8 月 1 日，OpenAI 一口气公布内部模型 Astra 的 10 项数学与理论计算机科学成果：非 sofic 群的存在性（Gromov 1999 年提出，悬了 27 年）、Connes 刚性猜想的反例、高维球体堆积新上界、算术电路计算 permanent 的下界、多色 Ramsey 数超指数下界等，覆盖 8 个领域，每一项都附带 Lean4 形式化证明证书，代码开源在 GitHub，两条命令就能编译验证。微博OpenAI 说这 10 个解花掉的 token 按 API 标价约 2000 美元，平均一个 200 美元。知乎
8 月 10 日，Anthropic 宣布其内部 Claude 模型在冲击黎曼猜想的过程中，把 ζ 函数非平凡零点落在临界线上的比例下界从 41.6% 推到了 67.2%，打破一个 37 年没人动的纪录。36氪注意：没有证明黎曼猜想本身，这是探索过程中的意外副产品，核心结果做了 Lean 形式化。
8 月 14 日前后，创业公司 CEO Lech Mazur 借助 AI 证明了约 70 年历史的森多夫（Sendov）猜想，陶哲轩随后发现这个证明实际上顺带解决了更强的 Phelps–Rodriguez 猜想。知乎
8 月 16 日，Lean 之父 Leonardo de Moura 的访谈流出，一句"我已经不写测试了，我写性质，AI 替我证明"传遍技术圈。知乎
然后就是今天的 Hopf：人类赢了，赢得干脆。
逐条核验：哪些实锤，哪些要让子弹飞
事件 | 验证状态 | 备注 |
|---|---|---|
Astra 十项成果 | 逻辑层实锤，内容层复核中 | 每项有 Lean4 证书，机器可查；但形式化语句是否精确对应原猜想，外部专家仍在逐条深究，官方也承认单项存在被撤回的可能 |
Connes 反例"被推翻" | 虚惊一场 | 所谓反驳来自一位三个月内"解决"三个千禧年难题的民科作者，论文发在哲学预印本站，社区查证后确认 OpenAI 反例没被推翻 |
Claude 黎曼下界 67.2% | 实锤但要限定 | Anthropic 官方发布，有专家检查和 Lean 形式化；但这是中间结果，离黎曼猜想本身还差得远 |
森多夫猜想 | 基本实锤，程序待走完 | 陶哲轩亲自背书并挖出更强结论；论文仍在同行评审流程里 |
Hopf 猜想（Brendle） | 预印本刚出 | 人类证明，用 Mathematica 做机器辅助但没用生成式 AI，等待社区复核 |
“SAB 解决 Hopf” | 无实锤 | 无官方声明、无预印本、无任何可查信源 |
六条里，真正"可以直接当定论"的其实没几条。这不是泼冷水，恰恰是这轮 AI 数学潮最值得看的地方：捷报的产能已经超过验证的产能，学会看验证状态，比学会刷新闻重要。
核验完，三个规律浮出来了
第一，AI 擅长"技巧融合"，弱于"结构发明"。
那 10 项成果里最有代表性的是量子并行重复（quantum parallel repetition）定理。一位以此为主业做了多年研究的学者花了一周逐行检查 Astra 的证明，结论是：它用的是标准框架，厉害之处在于把量子信息论、概率论、分析学多个子领域的技巧融合到一起并推到极致，“很难想象有一个人能同时精通这么多个子领域的技巧”。但他也直说：这些成果顶多是 STOC/FOCS 最佳论文的水平，够不着菲尔兹奖，而且领域专家一两周内就能彻底读懂。知乎这和菲尔兹奖得主 Timothy Gowers 的盘点也对得上：最近几个月最大的 AI 数学成果，几乎清一色是"找反例"或"构造特殊对象"类问题——雅可比猜想反例、Erdős 单位距离问题、非 sofic 群、多色 Ramsey 数。36氪这类问题可以化成"在巨大搜索空间里找一个满足条件的具体对象"，正是 AI 最擅长的活儿，试错成本不过是几千美元的 token。
再看 Hopf：证明的关键是设计一个前所未见的扰动结构，这恰恰是 AI 目前做不了的——GPT 试了几小时就放弃了。AI 能把已有的成熟技巧排列组合到极致，但"造出一个新结构"还是人类的活。这个分界线，可能是未来两三年判断"AI 数学新闻含金量"最实用的一把尺子。
第二，Lean 证书保的是"推导没错"，不保"题没审错"。
为什么现在每家 AI 实验室发数学成果都要附 Lean 证书？因为 AI 证明最怕的就是"看似合理的推导里悄悄跳一步"。Lean 编译通过，意味着每一步推导都被机器逐行检查过，这一层的错误被清零了。de Moura 自己说，Lean 的信任内核只有约 5000 行代码，小到任何人都能从零重写一遍来交叉验证。知乎但证书管不了两件事：一是形式化的语句是否精确捕捉了原问题的本意——陈述和猜想之间差一个字，证明的就是另一件事；二是可读性——此前 MathInc 的 Gauss 模型那份 20 万行的形式化证明，机器验证通过，人类却直批"不可审计"。微博至于"OpenAI SAB 解决 Hopf"这种连形式化都没有的传闻，按这套标准连入场资格都没有。
第三，专家复核的速度，目前还追得上 AI 出题的速度。
量子并行重复的专家用了一周，Connes 那场虚惊社区两三天就查证完毕。陶哲轩 6 月警告过"阻抗不匹配"——AI 生成正确证明的速度快到人类来不及审——但至少在这个 8 月，每一个大新闻都还接得住。微博真正的风险窗口，是未来 AI 开始批量产出深结构性证明的时候。
以后再刷到"AI 证明 XX 猜想"，照这三步走
有没有 Lean（或同类系统）形式化证书？没有的，先当故事听。
形式化的陈述是什么？证书只保证"证明了这个语句"，得确认这个语句就是原猜想。这次 Connes 风波和更早的单位距离猜想争议，争的都是这一层。
本领域专家复核了没有？看知乎、X 上该领域研究者的表态，比看官方博客可靠。专家说"两周内能彻底读懂"，是含金量很高的评价；专家沉默，就继续等。
接下来值得持续盯的三个信号：Astra 十项里有没有单项在深究后被撤回（官方自己留了这个口子）；Brendle 的 Hopf 证明能不能撑过社区复核——以及会不会有人把它搬进 Lean；"SAB"传闻到底是乌龙还是下一轮官方预告。
对关注 Lean 的人来说，这个 8 月真正的信号其实只有一个：Lean 已经从一小群人的证明工具，变成了 AI 数学成果的验收标准。所有想被当真的 AI 数学成果，都得过它这一关；而能看懂这张证书、能参与复核的人，就是这轮浪潮里最先上桌的人。捷报会越来越密，但判断力这东西，永远是稀缺品。
