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

这几周反例挺有趣的。这篇文章基本上是我对形式化、人工智能工具，尤其是反例领域动态的看法。

单位距离

两个月前的今天（2026年5月20日），ChatGPT 在离散几何中推翻了埃尔德什的单位距离猜想。 这已经是老生常谈了，但我总得从某处开始。 该公告伴随着人类数学家的证词， 其中许多人我认识，也有少数我信任，他们相信该论点（他们曾提前接触并核实过）。 该证明的基本结构是，1960年代戈洛德和沙法列维奇提出的数论中一个深刻定理可以用来构造该猜想的反例。

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

但不到一周后（2026年5月26日），我收到了菲尔兹奖得主迈克·弗里德曼的邮件。 迈克现任首席科学官逻辑智能这家公司由图灵奖得主、 “人工智能教父”严乐村共同创办。Mike告诉我，他们的系统已经自动形式化了整个ChatGPT生成的论文在精益模式中， 我可以看看吗？我查了，我的博士后Thomas Browning也看了。这正是逻辑智能所做的：他们正好形式化了数论深奥定理蕴含埃尔德什反例的陈述。 突破性的大型语言模型生成数学正在实时形式化。 有趣的数据点。

当然，这里有一个大问题，那就是数论的深刻定理，它需要100+页才能证明（它需要大量全局类域论， 这是20世纪初发展起来的理论，至今还没有简短的证明;压缩起来非常困难）。 2025年我主持了一件事克莱暑期学校与理查德·希尔一起研究类域论的形式化， 一年后我们几乎完成了局部案例（这是我学生谢爱迪生的当前博士项目）;全球论证依然悬而未决， 事实上，2025年将全局类域论形式化似乎成了幻想。

一个月后，2026年6月26日，我对可能性的看法再次发生了变化。 鲍里斯·阿列克谢夫在Lean Zulip上宣布他引导ChatGPT对埃尔德什反例进行了完全的形式化， 假设除了数学公理之外。Boris在OpenAI工作，他用他们的新模型Sol做了自形式化。 Boris公开了代码，我很快意识到，在这些AI生成（有时糟糕，但有时还算不错）的代码中， 确实是对全局类域论中一些非常难的定理的证明。 我还感兴趣的是，Sol在项目的三周内生成了120万行精益代码。 Lean的精彩数学库（利益冲突声明：我是维护者）Mathlib只有230万行代码， 花了九年时间编写。也许正是在这时，我真正意识到——大规模的人工智能数学发展是不可避免的。 AI生成的代码无法完全信任，所以我在自己的电脑上运行了沙盒（恶意的精益代码可以在你的电脑上运行任意命令——毕竟精益是一种编程语言）。 事实上，它正在证明关于数域上同调的非平凡定理。 哇。

阶为n的群方案

鲍里斯揭露真相一周后，也就是七月初，我认真思考如何管理我的费马工作坊形式化.本次研讨会由标志研究， 他们像逻辑智能（以及Harmonic、Axiom AI、Moonshot AI等）一样，拥有一种能够将数学自形式化的工具——将人类语言转化为精益——基于mathlib。 Logos告诉我，研讨会期间每次只能让5个人使用他们的系统，而当时有25名参与者， 所以我告诉所有参与者我会给他们买一个为期一个月的Claude Max订阅，这样他们在不轮到Logos工具的时候有东西可以尝试。 工作坊于7月6日至10日举行，Claude Max订阅将使参与者至少能使用Claude Fable，直到7日星期二关闭。当OpenAI得知我的做法后，他们还为所有与行者提供了一个月的免费ChatGPT Pro访问权限;这件事很重要，因为ChatGPT索尔将在9号发布。 所以基本上所有参与者在工作坊的五天里有四天可以使用Sol和Fable，并且整周都能使用Logos的工具。 事实上，Fable的通行权在7号并没有被取消，所以我们的状况更好。

我不确定Logos的工具会有多好，但我想在Lean中发展有限平坦群方案的理论， 用于我持续证明费马大定理，所以我把一些相关经典论文上传到Fable和ChatGPT， 并将它们汇聚起来用自然语言写下该理论的阐述。 我在研讨会前一天把这份PDF文件交给了Logos，研讨会第一天他们说PDF里的一个说法是错误的， 并且找到了一个明确的反例。又是一个反例！ 我查了一下，确实LLM生成的PDF在描述标准构造时确实有误;虚惊一场。 不过我自己在阅读PDF时也没注意到这一点。 有趣的是，人工智能又找到了反例。我修正了PDF。 我觉得有趣的是，AI并没有简单地说“我不太理解这个论点”，而是说“这里有证据证明这个论点根本错误”， 这句话更有说服力。

随着有限平坦群概形理论的发展步入正轨，我可以放松地回到FLT工作坊。 7月7日星期二，我坐在对面阿基尔·马修午餐时间;Akhil是芝加哥大学的数学教授， 他曾在场，正在尝试各种工具。我们讨论了人工智能可以解决的潜在问题，Akhil提出了Grothendieck的老问题： 是否每个阶n 的有限自由群方案都被 n 杀死。德利涅在交换情形中证明了结果，格罗滕迪克在基数约简时证明了结果;雷内·舒夫在更多案例中证明了这一点， 甚至还有一篇论文埃米利亚诺·托尔蒂去年发表， 更加普遍地证明了这一点。我说我觉得这是让人工智能思考的极好话题。

工作坊结束的第二天，也就是7月11日星期六，我收到了Akhil的私信，告诉我Sol找到了一个反例。 他给我发了一份12页的PDF。我立刻回复说我没有在看AI生成的非正式数学， 能否请他用精益语言形式化整个内容。四个小时后，他又回复说Fable已经把整个事情自形式化了。 我浏览了那个1076行的Lean文件，确认代码没有删除硬盘上的所有文件（Lean是一种编程语言， 所以可以这么做）。确信只是定理后，我用笔记本电脑整理了它，总共不到5分钟就检查了（a）所声称定理的陈述只用了mathlib中的概念（因此像这样）霍普代数可信其指数学家所说的霍普夫代数（b）声称定理的陈述是存在反例， （c）编制的证明。此时我知道我们有一个反例——一个阶为4的群方案，但没有被4阶结构破坏。 我建议阿基尔做个P......