2026年7月20日，帝国理工学院数学教授 Kevin Buzzard 在博客上写了一句直白到刺痛同行的话：人类数学家正在被「反例超越」。 原因是AI在短短两个月里，连续推翻了三道存在了数十年的数学猜想——其中一道悬而未决了将近一个世纪。
Buzzard 自己说：「我花了不到五分钟就验证完了一个60年未解的代数几何反例。把Lean代码下载到笔记本上，编译通过，然后点头说『是的，这确实是一个反例』。」
五分钟。这就是人类数学和AI数学的分界线。笔者今天想聊的是，这条分界线什么时候划下的，以及它意味着什么。
反例：一把比证明更锋利的刀
先讲一个基本概念。数学里，证明一个命题为真很难——你得写出一个严密到每一步都不能出错的推导。但证明一个命题为假，却相对「简单」：你只需要找到一个反例——一个满足所有前提条件却不满足结论的具体构造。
如果有人说「所有天鹅都是白的」，你不需要查遍全世界的每一只天鹅，只需要找到一只黑天鹅就够了。
一个反例，足以终结一个数学家毕生的研究。也正因为如此，反例在数学史上一直扮演着创造性的角色——它揭示理论的边界在哪，逼迫数学家重新审视假设、改进定义、推进理论。从某种角度说，反例是数学进步的燃料。
AI正在把这门「找黑天鹅」的技术推向一个不可思议的量级。
2026年5月到7月：AI的三连击
笔者按时间线梳理一下这三个月发生了什么。
第一击：Erdős 单位距离猜想（1946年提出，2026年5月20日被破）
传奇数学家 Paul Erdős 在1946年提出的离散几何问题。ChatGPT 给出了反例构造。Buzzard 的第一反应是问：「在 Lean 里验证了吗？」没有。但不到一周，菲尔兹奖得主 Mike Freedman（现为 AI 公司 Logical Intelligence 首席科学官）发来邮件——他们的系统已经把这套论证自动翻译成了 Lean 代码。
一个月后，OpenAI 的 Boris Alexeev 用新模型 Sol 完成了更彻底的工作：从数学公理出发，完整形式化了整个反例。Sol 为此生成了120万行 Lean 代码。
对比一下：Lean 社区花费九年写成的核心数学库 mathlib 总共只有230万行代码。AI 三周生成的量，就超过了人类九年积累的一半。Buzzard 的评语很简单：「大规模 AI 生成的数学发展已经不可避免。」
第二击：Grothendieck 群概形问题（1960年代提出，2026年7月11日被破）
Grothendieck 是20世纪最伟大的数学家之一。60年前他问了一个问题：n 阶的有限自由群概形是否一定被 n 消灭？Deligne 证明了交换情形成立，Grothendieck 自己证明了底环既约的情形成立——但完整结论一直悬着。
Sol 找到了一个反例。整个证明只有1076行 Lean 代码。Buzzard 花不到五分钟就全部验证通过。他建议数学家 Akhil Mathew 在数学库中提交这个反例——然后开玩笑说「你下一个要不试试 Hodge 猜想？」
第三击：雅可比猜想（1939年提出，2026年7月19日被破）
这是最重磅的一击。雅可比猜想（Jacobian Conjecture）是一个多项式映射的反问题：如果一个多项式映射的雅可比行列式是非零常数，那这个映射一定是可逆的吗？这个问题从1939年悬到现在，被称为代数几何中最诱人又最顽固的猜想之一。
这次出手的是 Anthropic 的 Claude Fable。它在2026年世界杯决赛期间找到了反例。第二天，陶哲轩——当代最受尊敬的数学家之一——就发了一篇博文，详细「消化」了这个反例的数学内涵。
陶哲轩的计算显示：这个反例是一个三变量、最高七次的多项式映射。它的雅可比行列式是 -2——满足非零常数的条件——但这个映射把三个不同的输入点映射到了同一个输出点，不是一一对应，因此不可逆。更令人惊叹的是，AI 用120个可以调节的参数，控制了雅可比行列式中理论上可能出现的1329项系数，让所有非零项恰好互相抵消。用陶哲轩的话来说：「这看起来像是一个巨大的奇迹。」
Lean + LLM：创意与铁证的联姻
讲完故事，笔者来提炼技术层面的逻辑。
Lean 是一个「数学编译器」。你用 Lean 写数学证明，每一行推理都必须通过严格类型检查。不存在「此处省略显然的步骤」——所有「显然」都必须展开到原子级别。如果代码通过编译，你的证明就是数学上绝对正确的——不依赖任何人类裁判的信任。
LLM（大语言模型）负责「构思」，Lean 负责「裁决」。LLM 做数学的固有弱点是它会胡编——明明不知道，也会写一段看起来像模像样的推理。Lean 的介入从根本上解决了这个问题：LLM 生成 Lean 代码，编译器立刻检查。如果编译不通过，LLM 收到错误信息后可以修正。反复迭代，直到代码通过编译——到这一步，AI 生成的数学结果就有了严格的正确性保障。
2026年3月，一篇题为《Learning to Disprove》的论文系统性地阐述了这套方法论。核心洞察是：与其让 LLM 去「证明」一个命题（容易胡编），不如让它去「找反例」——因为反例一旦用 Lean 编译通过，就铁证如山。论文作者采用了一种「符号变异」策略，从已有的定理中系统地删除某些条件，生成大量需要找反例的训练数据，然后用多奖励机制训练 LLM。实验结果是：在反例生成任务上，LLM 的准确率提升了49%。
这就是「反例超越」的技术基础：LLM 负责创意，Lean 负责铁证，人类数学家变成了观众——至少在结果验证这个环节。
数学界的「悲伤五阶段」
Buzzard 在博文中坦率地记录了他周围数学家的反应。他在帝国理工的午餐时间听到同事说：「反例这么容易找到，只是说明人类没有花足够时间去想这个问题。」他心中暗自苦笑——他自己曾经为这个「不值得花时间」的问题投入过整整一周。
这是典型的否认阶段。
紧接着就是讨价还价。有教授发邮件表示吃惊：为什么有研究生愿意每月花200美元订阅 Sol 和 Fable？Buzzard 的回复很直接：「任何不花这200美元的博士研究生才是不理性的。」哈佛大学已经为全体数学博士生、博士后和教员免费提供了 Fable 使用权限。
不管情感上能不能接受，一个事实是清晰的：在数学研究中，掌握 AI 工具的人和不掌握的人之间，能力差距正在以月为单位拉大。
陶哲轩给出的方向
在所有回应中，陶哲轩的姿态或许最值得关注。他没有去质疑 AI 的能力边界，也没有陷入「这还算不算数学」的哲学辩论。他坐下来，写了一篇详细的博文，算出了多项式的加权齐次性，给出了几何视角的重构，甚至贴出了他和 GPT-5 讨论的完整对话记录。
这是一种典型的一线数学家的态度：成果摆在那里，先理解它，再用它。
陶哲轩在 HN 上的讨论中指出：「它告诉我们，有些看似不可能的数学构造，在足够大的搜索空间中是可以被找到的。」这句话的关键隐藏信息是——搜索空间虽然巨大，但 AI 教会了我们搜索的方式。而这只是开始。
数学家还剩什么？
如果 AI 能找反例、能验证证明、能自动形式化完整理论，那数学家还剩什么？
Buzzard 给出的答案是：理解和解释。 他说：「这些非凡例子的真正价值，在于它们能带给人类对数学更深刻的理解。」Akhil Mathew 已经在尝试从更深的角度理解 Grothendieck 反例背后的结构——追问「这里真正发生了什么」，而非停留在「这是一个随机构造和一个巧合计算」。
AI 可以告诉你「它不成立」，但往往无法告诉你「这对我们的数学图景意味着什么」。
历史上，数学家一次又一次把「计算」外包给了机器，然后专注于更高层次的「理解」和「构造」。现在，「找反例」和「验证证明」也能外包了。剩下的人类工作恰恰可能是数学中最核心的部分：当机器把反例摆在桌上时，真正理解它为什么有意义——以及从中学到什么。
这不是数学的末日。但数学家的角色，确实在发生一场不可逆的进化。
参考链接：
- Xenaproject —— Kevin Buzzard 的原始博文「人类数学家被反例超越」
- HN 讨论（id: 48998362）—— 围绕陶哲轩雅可比猜想博文的社区讨论
- Lobsters 讨论（s/wfmpqr）—— 技术社区对 AI 数学反例的深度评论
- Terry Tao 的博文 —— 雅可比猜想反例的消化与数学重构
- SBSeminar —— 雅可比猜想新反例的数学细节讨论
- arXiv 2603.19514 —— Learning to Disprove：用大语言模型做形式化反例生成
- 新科学家杂志报道 —— AI 对87年数学难题的解答
- GitHub DeepMind Formal Conjectures —— 形式化猜想仓库，已收录雅可比反例
