你这两天大概被“AI跨过菲尔兹奖终点线”的新闻刷屏了。
先说结论：这次不是纯炒作，同一周发生的三件事里，确实有经过形式化验证的硬成果；但也不能整个吞下——722篇手稿里，目前完成机器核验的只有一百六十多篇，而且发布方是有翻车前科的。转发之前，值得花三分钟搞清楚哪些是真、哪些是半真、哪些只是标题。
第一件事：Claude悄悄证了一个70年没攻下来的猜想，这是本次最硬的成果
8月30日，2022年菲尔兹奖得主 Hugo Duminil-Copin 发了一篇略带忧伤的博客：在我们这个领域，最著名的那个猜想倒在推土机（AI）的轰鸣之下，恐怕只是个时间问题。他说的猜想，是渗流理论中的连续相变猜想，被称为概率论的“圣杯”。理解它可以想象冲咖啡：一张巨大的管道网格，每根管道有概率p畅通，p小了水渗不透，p大了会形成贯通的洪流，中间那个临界点就是“相变”。猜想问的是：恰好在临界点上，系统会不会凭空炸出一个无限大的连通网络？微博36氪
1957年 Broadbent 和 Hammersley 提出这个问题；1980年 Kesten 解决二维情形，奠定了他在数学史上的宗师地位；11维及以上被均场工具攻破；唯独3到10维——我们生活的物理宇宙所在维度——几十年无人撼动。Duminil-Copin 自己屡战屡败，失败的副产物反而帮他拿到了菲尔兹奖。微博
魔幻的是，博客发出几乎同时，同行们在 GitHub 上发现了 Anthropic 工程师提交的 anthropics/formal-math 代码仓库：没有发布会，没有官方博客，里面躺着由尚未公开发布的新一代 Claude 模型自动生成、经 Lean 形式化证明语言严格验证的完整证明代码。仓库README里写明的最终定理比新闻标题更彻底：θ(p_c)=0 对所有 d≥2 维成立——3到10维这些悬置的开放情形，被一次性打包解决了。GitHub
这条证明走的路，最后一块跳板是人类铺的：2024年 Kozma 和 Nitzan 发表论文，猜想了一组任意有限加权图上的“粘合不等式”，并证明其中最弱的猜想3直接蕴含 θ(p_c)=0。数学家们尝试构建辅助函数去证这个不等式，推导却总在关键节点产生奇异性崩溃，像条滑溜的泥鳅。而 Claude 在 Lean 证明助手的严苛约束下，用数千行形式化推理把它摁死了。下面这张图，就是那篇2024年论文里粘合不等式的几何设置示意。GitHub微博
数学界的反应分成几种。布伦瑞克工业大学的 Benedikt Jahnel 直言：如果是人类证明了这个猜想，大概率能拿菲尔兹奖，但现在是AI跨过了终点线。老将 Gil Kalai 谨慎表态：如果得到验证，这将是一项非凡的突破。宾夕法尼亚大学的 Ahmed Bou-Rabee 最务实——他借助大模型只花一天就泛化修改了证明代码，感慨自己苦做八年毫无进展的项目，如今距离彻底解决只有一步之遥。微博
最有意思的是铺下最后一块跳板的 Kozma 本人的态度：平静克制，暂不置评，等 Anthropic 发布“人类能看懂的版本”，并解释到底是怎么做到的。而 Anthropic 在仓库里的自我标注也很微妙：这是一份“静态研究工件”，不维护、不接受PR，正确性依靠 AUDIT.md 里记录的机器检查。记住这个细节，后面要用。微博GitHub
第二件事：OpenAI一夜甩出722篇手稿，数学圈却反应冷淡
10月6日21时47分（UTC），OpenAI 在 GitHub 创建了 openai/math 仓库，把722篇由内部未发布前沿模型生成的数学手稿一次性挂了上去，按372个结果族组织，涉及数论、代数几何、拓扑、理论计算机科学、数理逻辑等17个学科。创建一天多，星标就冲过了9500。GitHub
《华尔街日报》跟进报道点名的成果包括：朗道-西格尔零点排除、四维挂谷猜想的声称解、特殊情形的霍奇猜想。还有矩阵乘法：已证明的复杂度界从今年8月的约n^2.37降到约n^2.25，并配套了Lean形式化验证。微博微博
知乎上有人算了笔账：刚拿下本届菲尔兹奖的王虹与合作者十年磨一剑才解决三维挂谷猜想，而AI声称解决更难的4维版本只用了2周。高赞回答的观感是：菲尔兹奖可能真要成为人类最后一届了。知乎
但仓库自己的README比任何标题都清醒：“本合集包含处于不同验证阶段的结果，并非全部附有Lean形式化”。我数了仓库附带的形式化目录（formalization.yaml，v0.4）：目前列出“主定理已完成形式化”的论文只有162篇。生产线数据也已披露：平均每个结果消耗约3小时ChatGPT Pro推理算力，整个评估向模型提出了约4000道题。换句话说，绝大多数手稿眼下正处于没有机器核验的状态。GitHub微博
数学圈的反应，比舆论冷得多。知乎一个高赞回答说得直接：非常强，但数学界反应冷淡，之前的NS方程已经打了个底，现在这些成果除了量大管饱之外，并没有那么令人惊讶；更麻烦的是，数学家们不得不花大量时间去核验，却从中得不到新收获。这个“底”有必要展开：知乎
8月4日，OpenAI宣称攻破一道80年猜想，24小时内被数学家下场打回——不是证明错了，是“AI证对了每一句话，但已跟原猜想无关”。微博
9月8日，宣布用1万个AI智能体、88小时“攻克”千禧年难题纳维-斯托克斯方程，随后被指学术掠夺：纽约大学流体专家 Buckmaster 公开指责OpenAI向他施压，要求把一位在Anthropic工作的合作者从论文中剔除，他拒绝了。
9月11日，陶哲轩、邓煜等25位菲尔兹奖得主联名发表《人工智能在数学中的严重错位》，承认AI有加速研究的潜力，但反对仓促公布结果——来不及写论文、提炼新方法、引用在先工作。几天后，OpenAI撤回了对加州理工学院一项数学活动的赞助。微博
9月22日，OpenAI公布“独立数学审查小组”，阵容包括下一届国际数学联盟主席、美国和伦敦数学会主席。
10月3日，AI论文大爆炸冲击之下，arXiv启动史上最严限流。36氪
陶哲轩对722篇手稿这波的评价被广泛引用：前沿实验室的产出速度“太疯狂了”。注意，这是惊叹，不是背书——这批成果绝大多数尚未经过同行评审。微博
第三件事：和普通人关系最大的，其实是这条
同样在10月6日，数学家 Josh Alman 和 Virginia Vassilevska Williams 发布论文：用 Claude 发现了 3SUM 问题的 O(n^1.9992) 算法。同一篇论文把全源最短路（APSP）推到了 O(n^2.99942)，Anthropic 也已把这篇论文列入 formal-math 仓库的 Lean 形式化项目。这两个名字听起来陌生，但它们是复杂度理论的核心问题——一大类计算几何、数据库查询任务的效率下限都跟3SUM挂钩，下面这张图就是这批问题之间的归约关系网络。“真正次二次方”的3SUM是很多人此前不敢想的。相比“AI证明了某个猜想”，这类“AI帮忙发现新算法”离工程世界更近，也是你手里编码、Agent产品能力升级的上游信号。知乎GitHub
把三层证据分清，再决定投入多少情绪
第一层，机器核验过的。Claude的渗流猜想证明（Lean形式化+独立内核比对检查）、OpenAI目录里162篇完成主定理形式化的论文（含矩阵乘法新复杂度界）、正在形式化中的3SUM论文。这是目前最硬的部分。但“验证过”不等于“看懂了”——Kozma 要的“人类可读版本”还没出现，证明用了什么方法、对其他问题有没有价值，暂时没人说得清。
第二层，声称的成果。四维挂谷、特殊情形霍奇，以及722篇里其余大部分未形式化的手稿。挂在GitHub上，但README自己就写着：部分未形式化的结果可能存在问题。在独立审查小组给出结论前，把它们当成“待验证的高概率成果”比当成“已解决”更合适，毕竟还有8月4日“答错了题”的前科。GitHub
第三层，标题的包装。“跨过菲尔兹奖终点线”“准黎曼猜想被破”“AI几年内超越所有人类”。原始报道说的往往是“Lean验证的θ(p_c)=0证明”“朗道-西格尔零点排除”“某研究员的个人预测”，传到短视频里就变成了“AI打败了黎曼猜想”。情绪可以理解，但别把这一层当事实转发。36氪
这事跟你有什么关系？
先说不必恐慌的部分。知乎数学方向的答主早就说过大实话：解决猜想，短期内其实没啥现实应用，庞加莱猜想证明完十几年，也没见谁用上。“数学家失业”“人类倒计时”的叙事，多数是流量话术。真正的冲击在哲学层面——Duminil-Copin 说，一个数学问题绝不仅仅是一个等待被证明的定理，它不仅是黑夜里的灯塔，更是一个灵魂的导师，几十年的失败草稿孕育了几十个意想不到的新想法。AI把“结果”直接拿走了，但“过程”的价值还在人类这边，这正是25位菲奖得主联名信真正想守住的东西。知乎微博
再说对选AI工具的人有用的部分。你手里的订阅决策，不需要因为这条新闻改变。数学能力是模型推理能力的高地，Claude 和 OpenAI 这波竞速，早晚会下沉到编码、Agent、深度研究功能里；但决定续不续费的，仍然是你自己的使用场景、额度和价格，而不是谁家攻破了更多猜想。真要跟进，盯这几个信号比刷标题有用：Anthropic 会不会发渗流证明的人类可读版本、OpenAI 独立审查小组的首批结论、formalization.yaml 里162这个数字的爬升速度、arXiv 限流新政的落地情况、陶哲轩牵头“为数学界造AI”的后续。
以前看AI新闻是看产品发布会，这周开始，很多人第一次有了“见证科学史转折”的体感。转折是真的，但每个转折点上都挤满了贩卖焦虑的人。证明就在GitHub上，谁都能去看；喊得最响的那批，反而要多留个心眼。
