2026 年 7 月 20 日，帝国理工学院的 Kevin Buzzard 在 Xena Project 博客上发表了一篇标题直白的文章：《Human mathematicians are being outcounterexampled》。
这篇文章发表前两个月内，AI 系统连续推翻了数学史上多个重要猜想。Buzzard 用”outcounterexampled”这个词来描述一个正在发生的事实：人类数学家找反例的速度，已经跟不上机器了。
什么是”反例超越”？
“反例超越”是一个可以精确测量的现象。
Buzzard 本人是纯数学教授，也是 Lean 定理证明器社区的核心维护者。九年前，他经历了一场”中年危机”——不再信任人类数学家在处理技术细节时的准确性，转而投身形式化验证。他推动 Lean 进入数学教育，参与建设了拥有 230 万行代码的数学库 mathlib。
如今，让他写下这篇文章的，是两个月内密集发生的一系列事件。每次事件的结构几乎相同：AI 提出一个数学猜想反例，然后用 Lean 做出形式化验证，整个过程人类只是旁观者。
五月：Erdős 单位距离猜想
2026 年 5 月 20 日，ChatGPT 推翻了 Paul Erdős 在 1946 年提出的单位距离猜想。这是一个离散几何中悬而未决 80 年的问题。
OpenAI 的公告附带了多位人类数学家的证词——他们提前接触了论证过程，认为它是正确的。证明的核心结构是：用 Golod–Shafarevich 定理（1960 年代的一个深刻数论结论）来构造反例。
Buzzard 的第一反应是：“反例在 Lean 中形式化了吗？“答案是没有。
不到一周后的 5 月 26 日，菲尔兹奖得主 Mike Freedman 发来邮件。他现在是 Logical Intelligence 的首席科学官，这家公司由图灵奖得主、AI 教父 Yann LeCun 联合创立。Freedman 告诉 Buzzard，他们的系统已经将 ChatGPT 生成的论文自动形式化为 Lean 代码。
又过了一个月，6 月 26 日，事情再次升级。OpenAI 的 Boris Alexeev 使用新模型 Sol，将 Erdős 反例完整形式化——不依赖任何未经证明的公理，从数学公理出发完成了全部推导。Sol 为此生成了 120 万行 Lean 代码，耗时三周。
对比一下：mathlib——Lean 社区花九年时间写成的数学库——总共才 230 万行代码。
这个数字本身就是一个信号：AI 大规模生成数学内容已经不再是未来，而是现在。
Buzzard 在自己的机器上用沙盒运行了这些代码。代码确实在证明数域上同调中非平凡定理。他写道：“Wow。“
七月：Grothendieck 的群概形问题
Erdős 反例只是序幕。
7 月初，Buzzard 在伦敦帝国理工学院组织了一场”形式化费马大定理”工作坊（Formalizing Fermat workshop），由 Logos Research 赞助。参会者可以使用多种 AI 工具：Claude Fable、ChatGPT Sol，以及 Logos 自己的自动形式化系统。
工作坊期间发生了一起插曲：Buzzard 让 AI 撰写了一篇关于有限平坦群概形理论的综述，交给 Logos 的形式化工具处理。结果工具在一小时之内就发现 PDF 中有错误声明，并给出了一个明确的反例。Buzzard 后来修正了那篇 PDF。
有趣的是，AI 没有说”我不太理解这段论证”，而是说”这是一个证明，表明这段论证是错的”。这两种回应之间的差距，就是”反例超越”的核心。
7 月 11 日，工作坊结束次日，芝加哥大学教授 Akhil Mathew 给 Buzzard 发来消息：Sol 找到了 Grothendieck 在 60 年前提出的一个问题的反例。问题涉及”n 阶有限自由群概形是否被 n 消灭”——Deligne 证明了交换情形成立，Grothendieck 在底环既约时做了证明，Schoof 和后来的 Torti 不断推进，但完整结论始终悬而未决。
Sol 找到了一个阶为 4 的群概形，它不被 4 消灭。整个证明只有 1076 行 Lean 代码。
Buzzard 的验证流程很有意思：他先检查代码没有恶意操作（Lean 是编程语言，可以执行任意命令），确认它只包含定理，然后编译。整个过程不到五分钟，他就确认了三点：反例陈述只使用了 mathlib 中已有的数学概念、语句确实是反例、证明编译通过。
从收到消息到确认一个存在了 60 年的代数几何问题被推翻，不超过五分钟。
七月中旬：雅可比猜想
故事还没有结束。
7 月 19 日，同样是在 Mathew 的推动下，Levent Alpöge 在 X 上发布：Claude Fable 找到了雅可比猜想（Jacobian Conjecture）的反例。这是一个在代数几何领域开放了近 100 年的著名问题，无数数学家曾为之努力。
证明是在 2026 年世界杯决赛期间完成的。
当 Mathew 问 Buzzard”我是不是该提另一个 PR”时，已经晚了——Paul Lezeau 手动形式化了这个反例，并向 DeepMind 的 Formal Conjectures 仓库提交了 PR。
DeepMind 的仓库包含了大量形式化的猜想陈述。猜想的形式化是前提条件：一旦人类确认 Lean 语句准确捕捉了猜想的含义，那么验证 AI 生成的 Lean 代码是否构成证明或反例，就是一个机械过程。
社区的反应
Hacker News 上，这篇文章在 16 小时内获得了 360 分和 151 条评论。
一条高赞评论讲述了一个关于反例的经典故事：一位研究生在周五下午听到导师提出了一个猜想，导师希望它成立。整个周末导师都在尝试证明它。学生则花了全部精力寻找反例，一个小时内就找到了。学生写道：“我唯一一次对数学研究的贡献是一个反例，因为那是我唯一能做的事。”
另一位 HN 用户 veunes 评论说：“这大概是机器在反例方面表现如此出色的原因之一。它们对猜想没有美学承诺，对产生丑陋的东西也没有尴尬。”
这与 AlphaGo 战胜李世乭之后的讨论如出一辙：机器没有”美学下法”的概念，只要在法律框架内导向胜利，什么棋都敢走。
一些数学家的态度则更为复杂。Buzzard 在文章中提到，同事告诉他 Grothendieck 反例”太容易找到”，说明”人类没有花足够时间去思考这个问题”——暗示一个存在了 60 年的 Grothendieck 问题其实不值得研究。Buzzard 没有说出的是，他自己曾经花了一周时间在这个问题上。
“我的同事只是经历了悲伤的五个阶段，“Buzzard 写道，“现在他们似乎处在否认阶段。“
变革的代价
文章中的一个片段引发了激烈讨论。
Buzzard 提到，帝国理工的一位教授对研究生每月花 200 美元订阅 Sol 和 Fable 表示惊讶，认为这些学生”疯了”。Buzzard 的回应是：“任何不花这 200 美元的博士研究生才是疯了。”
评论区的 Jean Abou Samra 称这种态度”令人作呕”，认为这笔钱被用于”对后代犯下的巨大 V 形标志”——为数据中心建设更多燃气发电厂。Yemon Choi 也表示，不想看到这种心态在博士生中间被鼓励。
也有评论者从实用角度辩护：这些工具让研究者的生产力提升远不止 10%，200 美元是值得的投入。哈佛大学已经为所有博士生、博士后和教员免费提供 Fable 访问权限。
不管道德立场如何，一个事实是清晰可见的：在数学研究中，掌握 AI 工具的人和不掌握的人之间，差距正在以月为单位拉大。
形式验证的意义
这一系列事件中，Lean 定理证明器的作用不可忽视。
Lean 是一个交互式定理证明器和函数式编程语言，由 Leonardo de Moura 开发。它的核心功能是让数学证明可以被计算机形式化验证——每一行推理都必须通过类型检查，不存在”这里省略了显然的步骤”这种人类数学论文中的常见做法。
过去几年中，Lean 社区在数学形式化方面取得了显著进展：从 Abel–Ruffini 定理到塔尔斯基定理，从傅里叶分析到数论。2024-2025 年，AI 辅助的定理证明开始加速。OpenProver（2026 年 7 月的 arXiv 论文）展示了 Planner-Worker-Verifier 架构，AxiomProver 的多个智能体协同系统在 2026 年初解决了四个此前未解决的数学问题。
但 2026 年 5 月到 7 月的进展，无论在速度还是规模上都远超以往。
关键变化在于：AI 不只是辅助人类证明定理，它正在独立地发现数学事实并完全形式化它们。
数学的未来
这篇文章留下了一个开放的问题：当 AI 能比人类更快地找到反例、生成百万行级别的形式化证明时，数学家的角色是什么？
Madeleine Birchfield 在博客评论区提出了一个哲学问题：“当正式证明猜想的任务被外包给由大语言模型和证明助手组成的团队时，数学和数学家的意义是什么？当数学家不再需要亲手书写证明时，数学严谨性的意义又是什么？”
Buzzard 本人的态度更为务实。他在文章结尾写道，下一步是让人类理解这些例子的深层含义。“这些非凡例子的真正价值，在于它们能带给人类对数学更深刻的理解。“Akhil Mathew 已经在尝试从更深层次理解 Grothendieck 反例——追问”这里真正发生了什么”，而非停留在”这是一个随机环的随机表示和一个随机计算”的表层。
**反例超越是数学实践的一次根本性转移。**人类数学家的工作重心可能从”发现和证明”转向”理解和解释”。
这也许是 Buzzard 用”outcounterexampled”而非”replaced”的原因。机器正在超越人类找反例的速度，但理解这些反例背后的数学结构，仍然是——至少在 2026 年的夏天——人类的课题。
参考链接
- Kevin Buzzard, Human mathematicians are being outcounterexampled, Xena Project
- OpenAI, ChatGPT Sol 形式化 Erdős 反例公告
- Logical Intelligence, Freedman 联合创立公司公告
- DeepMind, Formal Conjectures 仓库
- Akhil Mathew, Grothendieck 群概形反例研究笔记
- Levent Alpöge, 雅可比猜想反例 X 帖子
本文的素材来自公开信息和社区讨论。如果你对这个话题有更深入的一手经验，欢迎指出文中的不足。
