最近几周，反例的情况非常有趣。这篇文章基本上是我对形式化、AI工具和特别是反例领域发生的事情的看法。单位距离两个月前的今天（2026年5月20日），ChatGPT在离散几何中驳斥了Erdős的单位距离猜想。这已经是陈旧的消息，但我必须从某个地方开始。这个公告伴随着一些人类数学家的证词，其中许多人我都认识，还有一些我所信任，他们表示他们相信这个论证（他们获得了提前访问权限并进行了检查）。证明的基本结构是，1960年代Gоlod和Shafarevich提出的一个深刻的数论定理可以用来构造对该猜想的反例。至今已经过去9年，自从我经历中年危机，意识到在技术细节上我不再信任许多人类数学家，发现了Lean，并开始争论交互式定理证明者应该在数学的未来中发挥重要作用。当时我第一个问题是“这个反例在Lean中是否被形式化？”答案是“没有”。但在不到一周后（2026年5月26日），我收到了Fields Medal获得者Mike Freedman的电子邮件。Mike现在是Logical Intelligence的首席科学官，这是一家由图灵奖得主和“AI教父”Yan LeCun共同创办的公司。Mike告诉我，他们的系统在Lean中自动形式化了整个ChatGPT生成的论文，我能否查看一下。我查看了，我的博士后Thomas Browning也查看了。确实这是Logical Intelligence所做的：他们准确地形式化了数论的深刻定理意味着Erdős反例的声明。突破性的大型语言模型生成的数学实时被形式化。这是一个有趣的数据点。当然，这里有一个显而易见的大问题——这个深刻的数论定理需要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的启示一周后，七月初，我正在认真思考如何运行我的Formalizing Fermat研讨会。这个研讨会由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日发布。因此，基本上所有与会者将在研讨会的五天中有4天可以访问Sol和Fable，整个一周都可以使用Logos的工具。实际上，Fable的访问并没有在……