AI攻克准黎曼猜想？数学家亲述震撼时刻

当AI开始证明数学猜想

在Lex Fridman的播客中，数论学家Alex分享了一个令他至今难以置信的时刻：他亲眼见证了准黎曼猜想（quasi-Riemann hypothesis）的证明被AI系统完成。这位研究黎曼猜想多年的专家坦言，他从未想过会在有生之年看到这一天。

消息发布时，Alex正在纽约参加美国国家数学博物馆的晚宴。他一手端着威士忌，一边不断刷新手机——因为他知道论文大约会在东部时间六点发布。当"quasi RH"字眼出现在屏幕上时，他的第一反应是困惑："你什么意思？准黎曼猜想？哪个函数的？"直到确认涉及Zeta函数和所有Dirichlet L函数，以及解决了no Zegel zeros相关问题，他才意识到自己看到的可能是一个历史性突破。

"那远远超出了我认知中可能性的边界。"他这样描述当时的感受。

一分钟理解黎曼猜想

对于不熟悉数论的读者，Alex给出了一个极简版本的解释。素数分布一直是数学的核心问题，而黎曼发现存在一个以复数为输入输出的函数——黎曼zeta函数——竟然支配着素数的行为。zeta函数的零点位置，也就是那些使输出为零的复数输入，决定了素数如何分布。

这个发现之所以令人震惊，在于它把离散的、不可分割的素数，与连续的复数空间联系了起来。Alex用信号处理做类比：就像麦克风把声波做傅里叶分析转换成振幅和频率，再由扬声器重建出人声，zeta函数对素数做的就是同样的信号处理分析。零点的频率和振幅信息，可以精确恢复出素数的分布。

而黎曼猜想预测的是：所有"黎曼波"的振幅完全相同——就像演奏素数音乐的管弦乐团中，每件乐器都以完全相同的音量发声。

什么是Dirichlet L函数？ 黎曼zeta函数只描述所有素数的整体分布，而Dirichlet L函数是它的推广：给定一个模q，L函数只“看到”模q某个剩余类中的素数。例如要研究形如4k+1与4k+3的素数是否各占一半，就需要用到模4的Dirichlet L函数。每个L函数都有自己的零点，广义黎曼猜想（GRH）断言这些零点也全部位于临界线上。准黎曼猜想的证明覆盖了Zeta函数和所有Dirichlet L函数，意味着它一次性处理了素数在任意等差数列中分布的深层规律，其影响远大于只针对单一zeta函数的结论。

什么是Siegel零点？ Siegel零点（也称Landau-Siegel零点）是指Dirichlet L函数在临界线附近、实轴上可能存在的异常零点。如果这种零点存在，会严重破坏素数在等差数列中的均匀分布，导致著名的“素数偏差”现象。数十年来数学家一直希望排除Siegel零点的存在，但始终未能做到。Alex提到的“no Siegel zeros”问题被解决，正是准黎曼猜想证明中最具分量的部分之一，因为它直接关系到素数分布最坏情形下的可控性。

一个月内三次认知颠覆

准黎曼猜想的证明并非孤立事件。Alex透露，这已经是他一个月内第三次被AI的能力震撼。

第一次是费马大定理的形式化。他曾在普林斯顿数学系做报告，详细解释Lean和mathlib的现状，并判断AI系统目前只能在现有库之上搭建一两层，擅长"杰里 rigging"式的修补，却做不好他所谓的"canonization"——即把粗糙代码重构、归位到库中规范位置的工作。他当时笃定，距离AI能形式化费马大定理至少还有三年。

结果报告是周三做的，周五就出现了1300万行的Lean代码，由Anthropic的AI系统生成了一个无sorry（即完整无漏洞）的形式化证明。"我说的每一句话都被证明是错的。"Alex说。

第二次是Navier-Stokes方程的进展，第三次就是准黎曼猜想。

Lean、mathlib与“sorry” Lean是一个交互式定理证明器，它把数学证明写成计算机可以逐行检查的代码。mathlib是建立在Lean之上的数学库，汇集了数以万计已形式化的定义与定理，是形式化数学的共同基础设施。在Lean中，sorry是一个占位符，表示“此处证明被跳过”。一个证明若含有sorry，就只是声明了结论而未真正验证；所谓“无sorry证明”，意味着每一行推理都被机器完整检查通过，中间没有任何未经证实的缺口。因此，1300万行无sorry的代码之所以震撼，是因为它代表了一个可被机器完全验证的费马大定理证明，而非仅仅是一份看起来合理的草稿。

形式化与canonization Alex区分了两种工作：一种是“jerry-rigging”，即用临时拼凑的代码把证明硬搭出来；另一种是“canonization”，即把粗糙代码重构、归位到mathlib的规范体系和命名约定中。前者只求跑通，后者才让代码可复用、可维护、可被后续证明依赖。AI目前擅长前者，后者仍需大量人工重构，这也是Alex强调“距mathlib质量还有大量工作”的技术含义。

不是优雅证明，但意义重大

Alex特别强调，AI生成的证明距离"mathlib质量"还有大量工作要做。它不是干净的证明，充满了临时拼接（jerry-rigging），需要大量重构和规范化。但他区分了两个层面的问题：如果目标是得到一个无sorry的形式化证明，那么自动形式化这个问题基本上已经解决了。

关于参与人数，据Alex了解只有两三位人类参与，且主要工作是"keep going"式的鼓励，没有领域专业知识介入。他也审慎地指出，从公司角度有动机把过程包装成"一句prompt就突破"，但实际训练中可能有哪些铺垫和未言明的步骤，外界并不清楚。

科学家也会说错话

面对如此快速的进展，Alex保持了科学家的坦诚："今天说的所有话中，40%到80%在五年后会被证明是错的。"他认为这正是人类讨论的价值所在——通过分歧、审议和话语交锋，科学过程本身就是在试错中前进，只是过去这个周期是十年、百年，现在被压缩到了几个月。

他形容这种感觉像是"哀悼"：自己多年积累的关于AI能力边界的经验模型被彻底打破，"它做X我信，做10X我不信，但这次是一百万X。"