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

最近几周，反例领域颇为热闹。本文主要分享我对形式化、AI工具，尤其是反例方面最新动态的一些看法。

单位距离问题

两个月前的今天（2026年5月20日），ChatGPT证伪了离散几何中的埃尔德什单位距离猜想。这已经是旧闻了，但总要找个切入点。声明发布时，附有多位人类数学家的证词——其中不乏我认识乃至信任的学者——表示他们相信这个论证（他们提前获得了论文并进行了验证）。证明的基本思路是，利用Golod和Shafarevich在1960年代证明的一个深刻的数论定理，可以构造出该猜想的反例。

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

但不到一周后（2026年5月26日），我收到了菲尔兹奖得主Mike Freedman的邮件。Mike现任Logical Intelligence首席科学官，这家公司由图灵奖得主、「AI教父」Yan LeCun联合创办。Mike告诉我，他们的系统已将ChatGPT生成的整篇论文自动形式化到Lean中，问我能否看看。我看了，我的博后Thomas Browning也看了。Logical Intelligence确实做到了：他们将那个数论深刻定理蕴含埃尔德什反例的命题形式化了。大语言模型生成的数学突破被实时形式化——这是个有趣的数据点。

不过这里有个显而易见的问题：那个数论深刻定理的证明长达100多页（需要大量全局类域论的内容——这是20世纪初发展的理论，至今没有简短证明，很难压缩）。2025年，我与Richard Hill合作举办了克莱数学夏季学校，主题是类域论的形式化。一年后的今天，我们几乎完成了局部情形（这是我学生Edison Xie当前的博士课题）；全局情形仍是开放问题，事实上2025年时形式化全局类域论看起来还像是天方夜谭。

一个月后的2026年6月26日，我对「可能性」的认知再次被刷新。Boris Alexeev