人类数学家正在被反例击败

过去几周，数学界经历了一场前所未有的震荡。一系列由人工智能驱动的反例接连出现，从Erdős的单位距离猜想，到Grothendieck关于n阶群方案的老问题，再到雅可比猜想——这些曾经被人类数学家反复推敲的经典命题，正在被AI逐一击破。这不是科幻小说，而是2026年夏天真实发生的数学史事件。

单位距离

两个月前的今天（2026年5月20日），ChatGPT宣布推翻了Erdős离散几何中的单位距离猜想。这条消息很快传遍数学圈，伴随而来的是多位人类数学家的证词——他们提前获得了论文访问权并进行了审查，认为论证是可靠的。证明的核心思路是：利用Golod和Shafarevich在20世纪60年代提出的一个深刻数论定理，构造出该猜想的反例。

对于熟悉形式化验证的人来说，一个自然的问题出现了：这个反例有没有在Lean中形式化？答案是“没有”——至少当时没有。九年前，我开始意识到交互式定理证明器应该在数学的未来中扮演重要角色，而信任人类数学家（尤其是在技术细节上）正变得越来越困难。但事情的发展速度远超预期。

不到一周后（2026年5月26日），菲尔兹奖得主Mike Freedman发来邮件。他所在的Logical Intelligence公司（由图灵奖得主、AI教*父Yann LeCun共同创立）已经用Lean自动形式化了整篇ChatGPT生成的论文。我让博士后Thomas Browning一起查看，确认了这一点：他们精确地将“数论定理蕴含Erdős反例”这一陈述形式化。大语言模型生成的数学，在实时中被形式化。这是一个值得注意的数据点。

当然，房间里还有一头大象：那个深刻的数论定理需要100多页的证明（涉及大量全局类域论，一种20世纪初发展起来的理论，目前没有简短证明，压缩十分困难）。2025年，我和Richard Hill一起办过一个克莱暑期学校，主题就是类域论的形式化。一年后，本地案例接近完成（这是博士生Edison Xie的当前项目），但全局案例仍然悬而未决——事实上，在2025年，形式化全局类域论看起来还像是一个幻想。

一个月后，2026年6月26日，可能性再次被刷新。Boris Alexeev在Lean Zulip上宣布，他引导ChatGPT完全形式化了Erdős反例，不依赖任何额外的数学公理。Boris在OpenAI工作，使用的是他们的新模型Sol。他公开了代码，而我在其中发现了全局类域论中一些非常困难的定理的证明。更令人震惊的是，Sol在三周内生成了120万行Lean代码——相比之下，Lean奇妙的数学库mathlib（利益冲突声明：我是维护者）总共只有230万行代码，却花了九年时间编写。正是在这一刻，我才真正意识到：AI驱动的数学大规模发展已经不可避免。当然，不能信任AI生成的代码，所以我在沙箱中运行了它（恶意Lean代码可以在你的电脑上执行任意命令——毕竟Lean是一种编程语言）。结果证明，它确实在证明关于数域上同调的非平凡定理。这真是令人惊叹。

n 阶群方案

Boris公布一周后，时间来到7月初。我正在认真筹备我主持的形式化费马研讨会（由Logos Research赞助，该公司拥有一套自动形式化数学的工具——将人类语言翻译成Lean，建立在mathlib之上）。Logos告诉我，研讨会期间只能同时允许5人使用他们的系统，而与会者有25人。于是我告诉所有参与者，我会给他们每人购买一个月的Claude Max订阅，以便在无法使用Logos工具时有所尝试。研讨会于7月6日至10日举行，订阅Claude Max后，与会者可以访问“Claude Fable”——至少7月7日之前该模型尚未被关闭。当OpenAI听说这件事时，也为所有参与者提供了一个月的免费ChatGPT Pro访问权限，这至关重要，因为ChatGPT Sol将于7月9日发布。因此，实际上所有参与者都能在5天研讨会中同时使用Sol和Fable，并在整个星期内使用Logos工具。Fable的访问权限在7日并未被撤销，所以情况比预期更好。

我不确定Logos的工具到底有多好，但我的目标是发展Lean中的有限平坦群方案理论，以便继续证明费马大定理。于是我将该领域的一些经典论文上传到Fable和ChatGPT，让它们合作用自然语言撰写该理论的阐述。我在研讨会前一天将这个PDF文档交给了Logos。研讨会第一天，他们告诉我PDF中有一个声明是错误的，并且找到了一个明确的反例——又一个反例！我检查后发现，确实是LLM生成的PDF在描述标准结构时出了错，虚惊一场。不过，我自己在阅读时也没有发现这个错误。有趣的是，AI再次找到了反例。我修正了PDF。值得注意的是，AI不仅仅说“我不太同意这个论点”，而是给出了一个证明论点完全错误的证据——这是一个更有力的声明。

随着有限平坦群方案理论的发展重回正轨，我可以安心回到FLT研讨会。7月7日星期二，午餐时我坐在Akhil Mathew对面。Akhil是芝加哥大学的数学教授，也是一位正在尝试现有工具的与会者。我们讨论了AI可以解决的潜在问题，他提出了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向mathlib提交一个PR——他照做了。我也建议他起草一份新闻稿，说机器解决了Grothendieck在代数几何中一个60年前的问题。但不知何故，此时我几乎对所有这些都免疫了。我不清楚媒体是否能区分“机器解决Erdős问题”和“机器解决Grothendieck问题”，尽管我个人觉得后者更有趣。当然，Grothendieck的反例比Erdős的反例简单得多（一千行代码对一百万行）。我想说的是，这是我个人认为更有趣的数学领域。我向Akhil指出，机器似乎越来越擅长寻找反例，并建议他下一步尝试霍奇猜想。

模块化提升定理

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

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

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

雅可比猜想

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

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

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

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