这几周的反例事件非常有趣。本文基本上是我对形式化世界、AI 工具以及反例领域最新进展的个人看法。

单位距离

两个月前的今天（2026 年 5 月 20 日），ChatGPT 否定了离散几何中的 Erdős 单位距离猜想。这已是旧闻，但我必须从这里开始。官方声明附带了多位人类数学家的证言，其中许多是我认识的，也有几位是我信任的，他们都表示相信这个论证（他们提前获得了访问权限并进行了检查）。该证明的基本结构是利用 20 世纪 60 年代 Golod 与 Shafarevich 提出的数论深刻定理来构造对该猜想的反例。

自从我九年前经历中年危机、意识到不再信任许多人类数学家的技术细节、发现 Lean 并开始主张交互式定理证明器应在数学的未来中发挥重要作用以来，“这个反例是否已在 Lean 中形式化”自然成为我的第一个问题。答案是“尚未”。

但不到一周后（2026 年 5 月 26 日），我收到菲尔兹奖得主 Mike Freedman 的邮件。Mike 现任 Logical Intelligence 首席科学官，该公司由图灵奖得主、“AI 教父” Yan LeCun 共同创立。Mike 告知我，他们的系统已将 ChatGPT 生成的整篇论文自动形式化到 Lean 中，并问我是否愿意查看。我查看了，博士后 Thomas Browning 也查看了。Logical Intelligence 确实做到了：他们精确地形式化了“该数论深刻定理蕴含 Erdős 反例”这一陈述。突破性的 LLM 生成数学成果正在实时被形式化。这是一个有趣的数据点。

当然，这里还有一头房间里的大象——那个需要 100 多页才能证明的数论深刻定理（它需要大量全局类域理论，而类域理论发展于 20 世纪初，至今仍无简短证明；压缩它非常困难）。2025 年，我与 Richard Hill 共同举办了 Clay 暑期学校，主题是类域理论的形式化；一年后，我们已接近完成局部情形（这是我的学生 Edison Xie 目前的博士课题）；全局情形仍未解决，实际上在 2025 年形式化全局类域理论仍显得像幻想。

一个月后，即 2026 年 6 月 26 日，我对可能性的认知再次发生改变。Boris Alexeev 在 Lean Zulip 上宣布，他引导 ChatGPT 完成了 Erdős 反例的完整形式化，仅依赖数学公理。Boris 就职于 OpenAI，使用了他们的新模型 Sol 来进行自动形式化。Boris 将代码公开，我很快意识到，在所有这些 AI 生成（有时糟糕，有时还算不错）的代码中，确实包含了对全局类域理论中一些极难定理的证明。同样令我感兴趣的是，Sol 在三周内生成了 120 万行 Lean 代码。而 Lean 优秀的（利益冲突声明：我是维护者之一）数学库 mathlib 仅有 230 万行代码，耗时九年才完成。也许正是在这一刻，我真正明白了——大规模 AI 生成的数学发展已不可避免。不能信任 AI 生成的代码，因此我在自己的机器上将其置于沙箱中运行（恶意 Lean 代码可以执行任意命令——毕竟 Lean 是一门编程语言）。确实，它正在证明关于数域上同调的非平凡定理。哇。

阶为 n 的群概型

Boris 发布消息一周后，7 月初，我正认真思考如何举办 形式化费马研讨会。该研讨会由 Logos Research 赞助，他们与 Logical Intelligence（以及 Harmonic、Axiom AI、Moonshot AI 等）一样，拥有可将数学从自然语言自动形式化到 Lean 的工具——基于 mathlib。Logos 告诉我，研讨期间他们将限制每次仅 5 人使用系统，而参会者有 25 人，因此我告诉所有参会者，我将为他们购买一个月 Claude Max 订阅，以便在轮不到使用 Logos 工具时也能进行实验。研讨会定于 7 月 6 日至 10 日举行，Claude Max 订阅将让参会者至少在 7 日周二之前访问 Claude Fable，当时它即将被关闭。当 OpenAI 得知我的计划后，也为所有参会者提供了一个月的免费 ChatGPT Pro 访问权限；这意义重大，因为 ChatGPT Sol 将于 9 日发布。因此，基本上所有参会者在研讨会的 5 天中将有 4 天能访问 Sol 和 Fable，以及整整一周的 Logos 工具。实际上，Fable 的访问权限并未在 7 日被移除，所以我们的条件甚至更好。

我当时不确定 Logos 的工具效果如何，但为了我正在进行的费马最后定理证明，我希望在 Lean 中发展有限平坦群概型理论，于是我将该领域的一些经典论文上传给 Fable 和 ChatGPT，让它们共同撰写一份自然语言的理论阐述。我在研讨会前一天将这份 PDF 文档交给 Logos，研讨会的第一天他们表示 PDF 中的一个断言是错误的，并给出了一个明确的反例。又一个反例！我查看后发现，LLM 生成的 PDF 在描述标准构造时确实有误；虚惊一场。不过我在阅读 PDF 时也漏掉了这一点。有趣的是，AI 再次找到了反例。我修复了 PDF。我觉得有趣的是，AI 并未只是说“我不太理解这个论证”，而是说“这里有一个证明，表明这个论证根本就是错的”——这是一个强大得多的陈述。

有限平坦群概型理论的发展重回正轨后，我得以在 FLT 研讨会上放松下来。7 月 7 日周二午餐时，我与 Akhil Mathew 相对而坐；Akhil 是芝加哥大学数学教授，也是一位参会者，他一直在尝试可用的工具。我们讨论了 AI 可能解决的问题，Akhil 提出了 Grothendieck 的老问题：阶为 n 的每个有限自由群概型是否都被 n 所杀死。Deligne 在交换情形下证明了该结果，Grothendieck 在基为约化时证明了它；Rene Schoof 在更多情形下证明了它，去年甚至有 Emiliano Torti 发表的 论文，在更一般的条件下证明了它。我说，我认为让 AI 思考这个问题非常棒。

研讨会结束后的第二天，即 7 月 11 日周六，我收到 Akhil 的私信，告诉我 Sol 找到了一个反例。他发来一份 12 页的 PDF。我立即回复说，我不会阅读 AI 生成的非形式化数学，请他将整个内容形式化到 Lean 中。四小时后，他再次回复说 Fable 已将整个内容自动形式化。我浏览了 1076 行的 Lean 文件，确认代码不会删除我硬盘上的所有文件（Lean 是一门编程语言，因此可以做到这一点）。确信这只是定理后，我在笔记本电脑上编译它，总共不到 5 分钟就检查出：（a）所声称定理的陈述仅使用了 mathlib 中的概念（因此 HopfAlgebra 等可以被信任为数学家所理解的 Hopf 代数）；（b）所声称定理的陈述是存在一个反例；（c）证明已编译通过。此时我确信我们找到了一个反例——一个阶为 4 却不被 4 杀死的群概型。我建议 Akhil 将该反例提交 PR 到 mathlib——他这样做了。我原本还想建议他起草一份新闻稿，宣布一台机器解决了代数几何中 60 年前的 Grothendieck 问题，但不知为何，此时我几乎已经对这一切免疫了。不清楚媒体是否能区分“机器解决了 Erdős 的问题”与“机器解决了 Grothendieck 的问题”，尽管我个人认为后者更有趣。当然，Grothendieck 反例远比 Erdős 反例容易（一千行而非一百万行），我只是想说这是我个人更感兴趣的数学领域。我向 Akhil 指出，机器似乎越来越擅长寻找反例，并建议他接下来尝试 Hodge 猜想。

模性提升定理

我认为此时有必要退一步，审视人类专家对这类事情的态度。7 月 14 日周二，我去帝国理工学院工作，Grothendieck 反例成了午餐的谈资。一位我不会透露姓名的教员对我说，反例如此容易被找到，只说明人类对这个问题思考得还不够，暗示 60 年前的 Grothendieck 问题其实并不值得投入兴趣。我没有告诉他，在我职业生涯的某个阶段，我曾花一周时间认真研究这个问题。在我看来，我的同事正在经历悲伤的五个阶段；现在他们似乎处于否认阶段。

午餐后，我与我的博士生 Andrew Yang 会面，他一直在用 Lean 形式化一个模性提升定理，这对我的 FLT 工作至关重要。Andrew 参加了 Logos FLT 研讨会，现在可以访问 Sol 和 Fable。他告诉我，使用这些工具，他在大概两周时间内编写了 25 万行 Lean 代码，基本上完成了整个项目。

几天前，我收到帝国理工学院数学系一位教授的邮件，他对我们的一些研究生每月支付 200 美元来访问 Sol 和 Fable 等模型表示惊讶。他说他认为这些人疯了。我当时没有立即回复。但在与 Andrew 会面后，我给那位教授回信，告诉他，在我看来，任何不支付 200 美元订阅这些工具的博士生才是疯了。实际上，在研讨会上，我从哈佛博士生 Bryan Wang 那里得知，哈佛已经为所有博士生、博士后和教员提供免费的 Fable 访问权限。

Jacobian 猜想

回到 Akhil。我不确定他是否认真对待我提出的反驳 Hodge 猜想的想法。但看起来他已深刻理解，借助这些非凡的新 AI 工具，反例目前可能是低垂的果实。他与 Levent Alpöge 讨论了在代数几何中寻找更多反例的想法，12 小时前，Levent 在 X 上发帖说 Fable 找到了 Jacobian 猜想 的反例。这是一个重大事件——这是一个著名的代数几何问题，已开放 100 年，许多人曾思考过它。据说它是在 2026 年世界杯决赛期间被解决的。

今天醒来，我收到 Akhil 的私信：“我应该再提交一个 PR 吗？”但这次他晚了一步——Paul Lezeau 已经手动形式化了该反例，并向 DeepMind 的 Formal Conjectures 仓库 提交了 PR。Mathlib 不包含大量数学猜想列表，但 DeepMind 的仓库包含。人类形式化猜想的重要性在于：如果人类一致认为 Lean 语句忠实地捕捉了猜想的含义，那么检查（可能是 AI 生成的）Lean 代码是否构成对该猜想的证明或反驳就变得微不足道。祝贺 Levent，感谢 Akhil 向他建议这个问题，也感谢 DeepMind 已经形式化了该语句，从而使反例的形式化验证变得微不足道。

Jacobian 猜想已解决！哇！接下来需要人类精确理解该例子到底发生了什么。因为这类工作的真正价值在于让人类更好地理解数学。实际上，Akhil 一直在尝试以比“这里是一个随机环的随机表示和一个随机计算显示某些东西不成立”更深的方式理解 Grothendieck 反例。我们接下来需要的是从这些非凡例子中得出的洞见。

多么精彩的时代。