AI面对黎曼猜想：它还会在哪些地方绊倒
摘要 黎曼猜想（RH）被普遍视为数学史上最重要的悬而未决难题之一。一个半世纪过去，它依旧让所有证明路线无功而返。随着人工智能逐步走入数学推理：能解竞赛题、能做复杂定理的检验、甚至能生成新的猜想——一个顺理成章的追问出现了：AI有没有可能证明黎曼猜想？若有，又需要满足哪些前提？
要回答它，我们不得不正视当下AI的短板、数学发现究竟依赖什么、形式化验证在其中扮演的作用，以及在证明能够被“认证”为无误之前必须搭建的巨型知识支架。下面将从三个互相缠绕的方向拆解：当前AI欠缺的关键能力、把解析数论搬进形式系统的浩大工程、以及足够强的AI是否可能完全绕过形式化这一关。
近些年数学AI的进展确实耀眼，但它们所能处理的层次，与黎曼猜想之间仍隔着巨大距离。下表概览了当今头部系统大致停留的高度。
这些成果主要对应“很强的本科生水平”或奥赛题目这类范围。黎曼猜想却属于另一种量级。问题不在于“换更快的机器”或“喂更多数据”，而在于：现阶段AI可执行的推理方式，与证明RH所需的推理质量之间存在断层式差距。
现有神经证明器，尤其是大语言模型，大多依赖对海量人类数学文本的统计与模式捕捉来学习，因而更像在已知前提与已知结论之间寻找过渡的“插值器”。但在训练语料里并不存在黎曼猜想的证明：没有哪条已写下的人类推理链能把ζ函数的定义一路连接到“全部非平凡零点都落在临界线”这一断言。若要成功，AI必须自己生成一份原创证明——向尚未被探索的数学区域做真正外推。这类能力，当前系统几乎没有展示过。
在象棋与围棋里，规则给出了封闭的状态集合，尽管空间庞大，却仍是可枚举的“封闭宇宙”。而在深层定理的证明中，“状态空间”包含一切可能的逻辑推导、定义引入与概念框架的选择。更关键的是，最决定性的那一步往往不是换一个已有招式，而可能是开辟一个新分支：也许借助随机矩阵的类比，也许发展基于自守形式的迹公式。潜在的新概念空间不仅极其宽广，而且高度开放。棋类中大显身手的蒙特卡洛树搜索与强化学习依赖于明确的动作集合与清晰的胜负信号；在黎曼猜想上，这两点都难以成立。
要证明RH，几乎必然需要长程的整体谋划：例如“用函数方程把问题压到临界带中的某个估计，再用光滑子技术处理，随后借助大筛不等式对相关和式给出界”，诸如此类。把高层目标拆成多层子任务，而且子任务本身可能还要求引入新定义与新工具——这种分层规划能力远超当今AI所能及。历史也反复表明，深刻证明往往伴随概念发明：格罗滕迪克为韦伊猜想发展概形；怀尔斯为费马大定理引入变形环。现阶段AI擅长拼装与重排既有材料，但尚未体现出能创造全新数学对象并洞察其用途的能力。
黎曼猜想并不属于离散组合或代数那种相对“离散化”的领域，它扎根于连续分析世界：极限与积分、复分析工具、以及带有微妙误差项的渐近估计。即便最强的自动证明器，对这类推理也常常束手无策。SMT求解器擅长实闭域，却处理不了超越函数层面的复杂性；计算机代数系统可以算数值，却无法直接证明涉及无穷集合的全局命题。AI在分析学细节面前通常更脆弱——弥补这块短板仍是根本性的研究难题。
为便于讨论，不妨先假设某位人类数学家（或某个AI）已经给出一份正确且严密的RH证明。若要达到确定性的最高标准——由Lean或Coq这类“可信内核”逐步检查的证明——就必须把每一步逻辑推导都形式化。这等价于：把现代解析数论的大部分装置完整翻译进证明助手的语言。
目前，形式化数学库（最具代表性的是Lean的mathlib）在代数、拓扑与测度论上积累深厚，但解析数论的覆盖仍相当有限。RH可能需要的背景——复分析中的诸多工具（Gamma函数、魏尔斯特拉斯乘积、Phragmén–Lindelöf定理）、整L函数理论、零点密度估计、大筛不等式、光滑子方法，甚至自守谱理论等——在库中几乎都缺位。
回看历史，最著名的大型形式化工程之一是用于验证开普勒猜想的Flyspeck项目，前后持续十余年、消耗约20人年。液体张量实验虽然结果更短、更自足，并且还能依托强大的既有代数库，仍需要专职团队投入18个月。若从头搭建解析数论体系，单靠人工可能以几十年为单位推进——很可能需要50到100人年甚至更高。难点不仅在于内容体量，更在于：形式化时必须显式处理带常数的渐近估计、严格证明极限与求和可交换、补齐分析学家在纸面上常省略的全部ε‑δ细节，其复杂度极高。
不过，这条时间线并非注定如此漫长。AI辅助形式化正在快速推进，并持续压缩成本。下表给出若干可能的未来情景，取决于AI参与程度与社区投入规模。
如今的大语言模型已经能够提出证明建议、把非形式化论证改写成形式化代码，并自动处理不少例行推导。“草稿—轮廓—证明”（Draft–sketch–prove）式流程允许人类把握整体路线，而让AI补齐机械细节。若这类工具持续迭代，一个资金充足、组织良好的协作计划，或许能把原本以几十年计的工程缩短到五到十年量级。形式化的边际成本正在快速下降。
更尖锐的问题在于：如果证明本来就是AI发现的，它是否还必须经受形式化这道“磨难”？答案很大程度取决于我们设想的是哪种AI形态。下表对两类主要设想作了对照。
一种未来图景是：AI吞下几乎全部非形式化数学文献——成千上万篇关于ζ函数、L函数与随机矩阵的论文——然后输出一份约200页的自然语言证明，由人类专家审读并判断其正确。在这种世界里，证明的发现阶段并不要求形式化；它会像怀尔斯证明费马大定理那样，经严格审查后被共同体接受。困难在于“信任”。当今大语言模型极擅长生成看似合理却可能虚假的内容。缺少形式化验证，我们只能像信任人类作者那样去信任AI，却缺乏人类直觉与问责机制作为补偿。对黎曼猜想这种精细而深邃的命题，数学界几乎必然会要求可机检的证明，以排除隐蔽错误——而这会立刻把问题拉回到形式化这座大山。
另一种图景是：AI成为AlphaProof一类系统的延伸，完全在证明助手内部开展推理。此时，AI的世界只包含库中已定义的概念与已证明的引理；它无法直接调用尚未形式化的分析估计。要让这种AI证明RH，相关解析数论内容必须事先以可操作的形式存在于系统中。此时形式化不再只是“验收环节”，而是AI推理本身赖以生存的环境。
最令人向往的长期愿景是：某个AI既能发现证明，也能同步把所需的新定义与新引理全部形式化。它能阅读非形式化论文，把其转化为形式理论，然后在这座新搭起的宏大基座上完成RH证明，一气呵成。在这一设想里，数十年的人力瓶颈将被抹平——形式化仍会发生，但由AI完成，耗时也许仅以月计。现阶段我们还没有这样的系统，但它指向了机器推理与形式证明深度融合的终点。
黎曼猜想不会因为对神经网络做几处巧调，或靠蛮力搜索就轻易被攻克。证明它很可能需要概念层面的跃迁、跨越多层的战略规划与精细的解析推理——这些恰恰是当今AI普遍缺乏的能力。即便某天找到了证明，想在证明助手里把它认证为无误，也意味着必须形式化解析数论的庞大版图；若缺少AI助力，这项工程可能绵延数十年。
但局面也并非凝固不动。工具每年都在变锋利。AI辅助形式化正在持续拉低构建数学库的门槛与成本。新的模型结构或许终将跨过从模式匹配到真正概念发明的鸿沟。而数学形式化也越来越像“目的地”而非“障碍”：一个通用、机器可读的数学知识库，在其中，黎曼猜想的证明——无论出自人类还是机器——都能被精确表达，并获得绝对确定性的检验。
机器今天还没准备好拿下黎曼猜想。但我们当下在更强证明器、更完善数学库与更聪明AI上所投入的努力，正是在铺设轨道：让未来那项也许最伟大的数学发现，能够在可验证、可托付的机制中安全到站。