人类数学家正在被反例超越

# 人类数学家正面临反例挑战 来源：https://xenaproject.wordpress.com/2026/07/20/human-mathematicians-are-being-outcounterexampled/ 过去几周对反例而言可谓精彩纷呈。本文主要从我个人的视角，梳理形式化领域、AI工具，尤其是反例方面的最新进展。 ## 单位距离 两个月前的今天（2026年5月20日），ChatGPT 在离散几何中否定了 Erdős 的单位距离猜想。这已经是旧闻了，但我必须从某个起点开始。与公告 (https://openai.com/index/model-disproves-discrete-geometry-conjecture/) 一同发布的是多位人类数学家的证词——其中不少我认识，也有几位我信任的人——他们声称相信这个论证（他们获得了早期访问权限并已核查过）。该证明的基本结构是：利用 Golod 和 Shafarevich 在1960年代提出的一个深刻的数论定理，可以构造该猜想的反例。 距我经历中年危机、意识到自己不再信任许多人类数学家处理技术细节的能力、发现 Lean 并开始主张交互式定理证明器应在数学未来中扮演重要角色，已经过去9年了。因此我的第一个问题自然是：“反例在 Lean 中形式化了吗？”答案是“没有”。 但不到一周后（2026年5月26日），我收到了菲尔兹奖得主 Mike Freedman 的邮件。Mike 现任 Logical Intelligence (https://logicalintelligence.com/) 的首席科学官，该公司由图灵奖得主、“AI 之父”Yan LeCun 联合创立。Mike 告诉我，他们的系统已将 ChatGPT 生成的论文全部自动形式化为 Lean 代码，希望我查看一下。我看了，我的博士后 Thomas Browning 也看了。确实，Logical Intelligence 做到了：他们将数论中那个深刻定理恰好形式化为能推导出 Erdős 反例的陈述。突破性的 LLM 生成数学实时形式化——有趣的数据点。 不过这里还有一个棘手的问题：那个深刻的数论定理需要100多页的证明（它依赖于20世纪初发展起来的全局类域论的大量内容，至今没有简短证明；压缩难度极大）。2025年，我与 Richard Hill 共同主办了一场 Clay 暑期学校 (https://www.claymath.org/events/formalizing-class-field-theory/)，主题是类域论的形式化。一年后，局部情形已接近完成（这是我学生 Edison Xie 当前的博士课题）；全局情形仍然开放，事实上在2025年，形式化全局类域论还像是天方夜谭。 一个月后，也就是2026年6月26日，我对可能性的认知再次被颠覆。Boris Alexeev 在 Lean Zulip (https://leanprover.zulipchat.com/#narrow/channel/583339-AI-authored-projects/topic/Erd.C5.91s.20unit-distance.20counterexample.2C.20exponent.20above.201/near/606778508) 上宣布，他引导 ChatGPT 完整形式化了 Erdős 反例，且不依赖任何数学公理之外的前提。Boris 在 OpenAI 工作，他使用了他们的新模型 Sol 进行自动形式化。Boris 公开了代码，我很快发现，在这堆 AI 生成的（有时很糟糕，有时还行）代码中，确实包含了全局类域论中一些非常困难的定理的证明。此外令我感兴趣的是，Sol 在为期三周的项目中生成了120万行 Lean 代码。而 Lean 出色的数学库 mathlib (https://github.com/leanprover-community/mathlib4) 总共只有230万行代码，却花了九年时间编写。也许正是在这一刻，我才真正意识到：大规模 AI 生成的数学发展不可避免。AI 生成的代码不可信，所以我在一台沙盒机器上运行了它（恶意的 Lean 代码可以在你的计算机上执行任意命令——毕竟 Lean 是一种编程语言）。果然，它证明了关于数域上同调的非平凡定理。哇。 ## n 阶群概形 在 Boris 公布结果一周后，7月初，我正绞尽脑汁思考如何运行我的“形式化费马大定理工作坊” (https://xenaproject.wordpress.com/2026/05/15/formalizing-fermat-workshop/)。该工作坊由 Logos Research (https://www.logosresearch.ai/) 赞助，这家公司（与 Logical Intelligence、Harmonic、Axiom AI、Moonshot AI 等一样）拥有一个基于 mathlib 将数学从人类语言自动形式化为 Lean 的工具。Logos 告诉我，工作坊期间他们的系统每次只允许5人使用，而参加者有25人，所以我告知所有参加者，我会为他们购买一个月的 Claude Max 订阅，这样在非轮到使用 Logos 工具时，他们也能有东西可以实验。工作坊于7月6日至10日举行，Claude Max 订阅可以让参加者访问 Claude Fable，至少到7月7日星期二（届时该模型将被关闭）。OpenAI 得知我的做法后，也主动为所有参加者提供一个月免费的 ChatGPT Pro 访问权限；这很重要，因为 ChatGPT Sol 将在7月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 (https://math.uchicago.edu/~amathew/) 共进午餐；Akhil 是芝加哥大学的数学教授，也是一位尝试使用各种工具的参加者。我们讨论了 AI 可以研究的潜在问题，Akhil 提出了 Grothendieck 的一个老问题：是否每个 n 阶有限自由群概形都被 n 杀死？Deligne 已经证明了交换情形，Grothendieck 证明了底概形约化时的情形；Rene Schoof 证明了更多情形，甚至去年 Emiliano Torti 发表了一篇论文 (https://ems.press/content/serial-article-files/51994)，将结论推广到更一般的情形。我说我认为这是一个让 AI 思考的绝佳问题。 工作坊结束后的第二天，7月11日星期六，我收到了 Akhil 的私信，告诉我 Sol 找到了一个反例。他发给我一份12页的 PDF。我立即回复说我不读 AI 生成的非形式化数学，请他把整个东西在 Lean 中形式化。四个小时后他再次回复，说 Fable 已经自动形式化了整个内容。我快速浏览了1076行的 Lean 文件，检查代码是否会删除我硬盘上的所有文件（Lean 是一种编程语言，确实可以做到）。确认只有定理后，我在笔记本电脑上编译了它，总共用了不到5分钟就验证了：(a) 声称定理的陈述仅使用了 mathlib 中的概念（因此像 `HopfAlgebra` 这样的东西可以信赖为数学家心目中的 Hopf 代数含义）；(b) 定理的陈述说的是存在一个反例；(c) 证明编译通过。此时我意识到我们确实有了反例——一个阶数为4、不被4杀死的群概形。我建议 Akhil 向 mathlib 提交一个包含该反例的 PR——他照做了 (https://github.com/leanprover-community/mathlib4/pull/41748)。我本想建议他也起草一份新闻稿，宣称机器解决了一个代数几何中 Grothendieck 提出的60年未解问题，但不知为何到这时我已经对这一切几乎免疫了。我不确定媒体能否区分“机器解决了 Erdős 问题”和“机器解决了 Grothendieck 问题”，尽管我个人觉得后者有趣得多。当然，Grothendieck 反例远比 Erdős 反例简单得多（一千行 vs 一百万行），我只不过是想说，这个数学领域我个人觉得更有意思。我向 Akhil 指出，机器似乎在寻找反例方面越来越厉害，并建议他接下来试试 Hodge 猜想。 ## 模性提升定理 我想此时有必要退一步，审视一下人类专家对这些事情的态度。7月14日星期二，我去帝国理工学院上班，午餐时 Grothendieck 反例成了话题。一位教职员工（我不点名）对我说，反例如此容易找到，只说明人类在这个问题上花的时间还不够多，言下之意是 Grothendieck 那个60年的问题实际上并不值得研究。我没有告诉他，在我职业生涯早期曾花了一周时间努力钻研这个问题。在我脑海里，我的同事只是正在经历悲痛的五个阶段；目前他们似乎处于否认期。 午饭后我见了我的博士生 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 (https://x.com/__alpoge__/status/2079028340955197566?s=20) 上发帖称，Fable 找到了 Jacobian 猜想 (https://en.wikipedia.org/wiki/Jacobian_conjecture) 的一个反例。这可是个大新闻——这是代数几何中一个著名的开放问题，已有100年历史，无数人思考过。据说它是在2026年世界杯决赛期间被解决的。 今天早上我醒来时收到 Akhil 的私信：“我再提一个 PR 吗？”但这次他晚了——Paul Lezeau 已经手动将反例形式化，并向 DeepMind 的 Formal Conjectures 仓库 (https://github.com/google-deepmind/formal-conjectures) 提交了 PR (https://github.com/google-deepmind/formal-conjectures/pull/4474)。Mathlib 中并未包含大量数学猜想，但 DeepMind 的仓库有。人类将猜想形式化的意义在于：如果人类一致认为某个 Lean 陈述确实忠实捕捉了猜想背后的思想，那么验证（可能是 AI 生成的）Lean 代码是否构成该猜想的证明或否证就变得微不足道。祝贺 Levent，感谢 Akhil 向他提出这个问题，也感谢 DeepMind 已经形式化该陈述，从而使得反例的形式化验证变得轻而易举。 Jacobian 猜想解决了！哇！下一步工作是让人类理解这个例子的确切机制。因为这类工作真正的价值在于让人类更深入地理解数学。确实，Akhil 一直在努力以远不止“这是一些随机的环表示和一些随机计算，表明某些东西不成立”的方式理解 Grothendieck 反例。我们接下来需要的是从这些非凡例子中提炼出的洞察。 活在这个时代真好。