人类数学家正被反例击败

对于反例来说，这几周是很有趣的。这篇文章基本上是我对形式化、人工智能工具，特别是反例领域正在发生的事情的看法。

单位距离

两个月前的今天（2026 年 5 月 20 日），ChatGPT 反驳了 Erdős 离散几何中的单位距离猜想。现在这已经是旧闻了，但我必须从某个地方开始。该声明附有人类数学家的证词，其中许多人是我认识的，其中一些是我信任的，他们说他们相信这个论点（他们已经获得了早期访问权并进行了检查）。证明的基本结构是，Golod 和 Shafarevich 在 20 世纪 60 年代提出的一个深刻的数论定理可以用来构造该猜想的反例。

距离我经历中年危机、意识到在技术细节方面我不再信任许多人类数学家、发现精益并开始认为交互式定理证明器应该在数学的未来中发挥重要作用，已经过去了 9 年。所以我的第一个问题当然是“精益中的反例是否形式化”。答案是“不”。

但不到一周后（2026 年 5 月 26 日），我收到了菲尔兹奖得主迈克·弗里德曼 (Mike Freedman) 发来的电子邮件。 Mike现任逻辑智能公司首席科学官，该公司由图灵奖获得者、“人工智能教父”颜乐存共同创立。 Mike 告诉我，他们的系统已经在 Lean 中自动形式化了整个 ChatGPT 生成的论文，我可以看一下吗？我看了看，我的博士后托马斯·布朗宁也看了。事实上，这就是逻辑智能所做的：他们精确地形式化了这样的陈述：数论的深刻定理隐含着埃尔多斯的反例。突破性的大语言模型生成的数学被实时形式化。有趣的数据点。

当然，房间里有一头大象，那就是需要 100 多页纸才能证明的深刻的数论定理（它需要大量的全局类场论，这是一种在 20 世纪初发展起来的理论，目前还没有简短的证明；事实证明很难压缩）。 2025年，我和Richard Hill一起办了一个克莱暑期学校，主题是类场论的形式化，一年后我们几乎完成了本地案例（这是我的学生Edison Xie目前的博士项目）；全球案例仍然悬而未决，事实上，到 2025 年，正式化全球阶级场论似乎是一个幻想。

一个月后，即 2026 年 6 月 26 日，我对可能性的看法再次发生了变化。 Boris Alexeev 在 Lean Zulip 上宣布，他已经引导 ChatGPT 完全形式化了 Erdős 反例，除了数学公理之外没有任何假设。 Boris 在 OpenAI 工作，并使用他们的新模型 Sol 来进行自动形式化。鲍里斯公开了代码，没过多久我就意识到，在所有这些人工智能生成的（有时是可怕的，但有时是不错的）代码中的某个地方确实是全局类场论中一些非常困难的定理的证明。我还感兴趣的是，Sol 在该项目的三周内生成了 120 万行精益代码。 Lean 的奇妙的（利益冲突声明：我是维护者）数学库 mathlib 只有 230 万行代码，花了九年时间编写。也许正是在这一点上，我才真正放下心来——人工智能带来的数学的大规模发展是不可避免的。人们不能信任人工智能生成的代码，因此我在我的机器上的沙箱中运行它（恶意精益代码可以在您的计算机上运行任意命令 - 毕竟精益是一种编程语言）。事实上，它正在证明关于数域上同调的非平凡定理。哇。

n 阶群方案

鲍里斯透露一周后，即七月初，我正在认真思考如何举办我的形式化费马研讨会。本次研讨会由 Logos Research 赞助，该公司与 Logical Intelligence（以及 Harmonic 和 Axiom AI 以及 Moonshot AI 等）一样，拥有一种可以自动形式化数学的工具——将其从人类语言翻译成 Lean——建立在 mathlib 之上。 Logos 告诉我，在研讨会期间，他们一次只允许 5 个人使用他们的系统，而与会者有 25 人，所以我告诉所有与会者，我会给他们购买一个月的 Claude Max 订阅，这样当轮不到他们使用 Logos 的工具时，他们就有了一些可以尝试的东西。研讨会于 7 月 6 日至 10 日举行，订阅 Claude Max 后，与会者可以访问《Claude Fable》，至少在 7 日星期二之前，该网站将被关闭。当 OpenAI 听说我正在做的事情时，他们还为所有与会者提供了一个月的免费 ChatGPT Pro 访问权限；这是一件大事，因为 ChatGPT Sol 将于 9 日发布。因此，基本上所有与会者都可以在 5 天的研讨会中使用 Sol 和 Fable，并在整个星期内使用 Logos 工具。事实上，《神鬼寓言》的访问权限在 7 日并未被删除，所以我们的状况甚至更好。

我不确定Logos的工具有多好，但我想在精益中发展有限平坦群方案的理论，以便我不断证明费马大定理，所以我把该领域的一些经典论文上传到Fable和ChatGPT，并让他们一起用自然语言写下该理论的阐述。我在研讨会前一天将这个 pdf 文档传递给了 Logos，在研讨会的第一天，他们说 pdf 中的一个声明是错误的，并且他们找到了一个明确的反例。又一个反例！我看了一下，确实，LLM 生成的 pdf 在描述标准结构时有时是错误的；虚惊。不过，我在阅读 pdf 时错过了这一点。有趣的是人工智能如何再次找到反例。我修好了pdf。我认为有趣的是，人工智能不仅仅说“我不太同意这个论点”，而是说“这是一个证明这个论点完全错误的证据”，这是一个更有力的声明。

随着有限平坦群方案理论的发展回到正轨，我可以放松地回到 FLT 研讨会。 7 月 7 日星期二，午餐时我坐在 Akhil Mathew 对面。阿基尔是芝加哥大学的数学教授，他是一位与会者，一直在尝试现有的工具。我们讨论了人工智能可以解决的潜在问题，阿基尔提出了格洛滕迪克的老问题：是否每个 n 阶有限自由群方案都被 n 杀死了。德利涅证明了交换情况下的结果，格洛腾迪克证明了基数减少时的结果； Rene Schoof 在更多案例中证明了这一点，甚至去年 Emiliano Torti 发表的一篇论文也更普遍地证明了这一点。我说我认为让人工智能思考这是一件很棒的事情。

研讨会结束后的第二天，也就是 7 月 11 日星期六，我收到了 Akhil 发来的私信，告诉我 Sol 找到了一个反例。他给我发了一份 12 页的 pdf 文件。我立即回复说，我没有阅读人工智能生成的非正式数学，请他用精益形式形式化整个事情。四小时后，他再次回复，说《神鬼寓言》已经将整个事情自动形式化了。我扫描了 1076 行 Lean 文件，检查代码没有删除我硬盘上的所有文件（Lean 是一种编程语言，所以它可以做到这一点）。我确信这只是定理，然后在我的笔记本电脑上编译它，总共花了我不到 5 分钟的时间来检查 (a) 所声称的定理的陈述仅使用 mathlib 中的概念（因此像 HopfAlgebra 这样的东西可以被相信表示数学家所认为的 Hopf 代数） (b) 所声称的定理的陈述是有一个反例，以及 (c) 编译的证明。此时我知道我们有一个反例——一个 4 阶群方案，没有被 4 杀死。我建议 Akhil 用反例向 mathlib 做一个 PR——他这么做了。我还建议他起草一份新闻稿，说机器已经解决了格洛腾迪克在代数几何中的一个 60 年前的问题，但不知何故，此时我几乎对所有这些都免疫了。我不清楚媒体是否能够区分“机器解决埃尔多斯的问题”和“机器解决格洛腾迪克的问题”，尽管我个人发现后者更有趣。当然，格洛腾迪克的反例比埃尔德的反例要简单得多（一千行，而不是一百万行），我想说的是，这是我个人认为更有趣的数学领域。我向阿基尔指出，机器似乎越来越擅长寻找反例，并建议他接下来尝试霍奇猜想。

模块化提升定理

我认为此时值得退后一步，调查一下人类专家对此类事情的态度。周二（7 月 14 日）我去帝国理工学院上班，午餐时谈论的就是格罗腾迪克的反例。一位教授（我不会透露他的名字）对我说，反例如此容易找到，恰恰表明人类没有花足够的时间思考这个问题，这意味着格罗腾迪克的一个 60 年前的问题实际上并没有那么有趣。我没有告诉他，在我职业生涯早期的某个时刻，我花了一周的时间努力解决这个问题。在我看来，我的同事正在经历悲伤的五个阶段；现在他们似乎正处于否认阶段。

午餐后，我会见了我的博士生 Andrew Yang，他一直致力于将精益中的模块化提升定理形式化，这对我的 FLT 工作至关重要。 Andrew 来到了 Logos FLT 研讨会，现在可以访问《Sol》和《神鬼寓言》。他告诉我，他使用这些工具编写了 25 万行精益代码，我猜这需要 2 周的时间，基本上完全完成了该项目。

几天前，我收到了帝国理工学院数学系一位教授的一封电子邮件，他对我们的一些研究生每月支付 200 美元来访问 Sol 和 Fable 等模型表示惊讶。他说他认为这些人疯了。我没有立即回应。但在与安德鲁会面后，我给教授发了一封电子邮件，告诉他在我看来，任何不每月支付 200 美元来访问这些工具的博士生都是疯狂的。事实上，在研讨会上，我从哈佛博士生 Bryan Wang 那里了解到，哈佛已经向哈佛的所有博士生、博士后和教师免费提供《寓言》。

雅可比猜想

但回到阿基尔。我不确定他是否认真对待我反驳霍奇猜想的想法。但看起来他已经深刻认识到，有了这些非凡的新人工智能工具，反例现在可能是唾手可得的成果。他曾与 Levent Alpöge 讨论过在代数几何中寻找更多反例的想法，12 小时前，Levent 在 X 上发帖称《寓言》找到了雅可比猜想的反例。这是一件大事——这是代数几何中的一个著名问题，这个问题已经开放了 100 年，很多人都在思考这个问题。这个问题显然在2026年世界杯决赛期间得到了解决。

今天我醒来时，Akhil 发来一条私信，问我“我可以再做一次公关吗？”但这一次他来得太晚了——Paul Lezeau 已经手动形式化了反例，并对 DeepMind 的 Formal Conjectures 存储库做了 PR。 Mathlib 不包含大量数学猜想，但 DeepMind 的存储库包含大量数学猜想。人类猜想形式化的重要性在于，如果人类一致认为精益陈述确实忠实地捕捉了猜想背后的想法，那么检查（可能是人工智能生成的）精益代码是否包含对猜想的证明或反驳就变得微不足道了。恭喜 Levent，感谢 Akhil 向他提出问题，感谢 DeepMind 已经将声明形式化，从而使反例的形式验证变得轻而易举。

雅可比猜想解决了！哇！这项工作的下一步是让人们准确理解这个例子到底发生了什么。因为这样的工作的真正价值在于让人类更好地理解数学。事实上，阿基尔一直致力于以一种比“这是一个随机环的随机呈现和一个表明某些东西不起作用的随机计算”更深层次的方式来理解格洛腾迪克反例。接下来我们需要的是从这些非凡的例子中得出的见解。

活着是多么美好的时光啊。