把大象放进冰箱：论用计算方法逼近黎曼猜想

作者：李昂（Ang Li）

Phaenarete Project · 广州菲娜睿特人工智能科技有限责任公司

2026 年 5 月

摘要

希尔伯特在 1900 年提出的 23 个问题中，第八问题包含黎曼猜想。一百二十六年后的今天，这个猜想仍在挑战人类理性的边界。本文面向形式科学（数学、逻辑学、哲学、理论计算机科学）的研究者，系统阐述一种用计算方法逼近黎曼猜想的路径。这一路径的核心思想是：将黎曼猜想等价转化为一台具体的小型图灵机的停机问题，并在"可观测"的范围内研究其计算行为。我们将回顾从 Yedidia-Aaronson 到 Matiyasevich、再到 O'Rear 的关键进展——黎曼猜想已被编码为仅有 744 个状态的图灵机。在此基础上，我们提出"ZetaHalt"项目：不企图在经典的确定型计算中穷举搜索，而是建立数据驱动的、人机协同的观测与实验平台，用机器学习模型学习这台机器的行为模式，用可解释性工具提取候选数学不变量，并用形式化验证系统（Lean 4）进行严格检验。本文还将讨论这一研究路径的哲学意义：它改变了"证明"与"理解"的关系，也为形式科学中"不可判定"与"不可知"之间的边界提供了可量化的实验场。

关键词：黎曼猜想；希尔伯特第八问题；图灵机；停机问题；忙碌海狸；ZetaHalt；形式化验证；数学实验

1. 引言：希尔伯特的第八问题与我们时代的新工具

1900 年 8 月 8 日，大卫·希尔伯特在巴黎国际数学家大会上发表了他那篇改变数学史的演讲。他提出的 23 个问题中，第八问题涵盖数论中若干核心猜想，其中影响最深远的——用希尔伯特自己的话来说——"或许是最重要的"——是关于黎曼ζ函数非平凡零点的猜想。

黎曼本人在 1859 年的八页论文中提出了这个猜想，然后轻轻带过一句："经过一番短暂而徒劳的尝试后，我暂时将其搁置。"一个半世纪以来，这个"暂时"变成了数学史上最漫长的等待。

为什么这个问题如此困难？一个根本性的原因是：黎曼猜想连接着两种看似不相容的数学结构。一方面是素数——离散的、顽强的、拒绝被简单公式捕捉的整数。另一方面是ζ函数的零点——连续的、分析的、深嵌于复变函数论的精密结构。黎曼猜想断言这两者之间存在一种精确的对应关系。要证明它，必须在这两座大山之间架设桥梁。

传统的方法——从哈代（1914）证明临界线上有无穷多零点，到塞尔伯格（1942）证明正比例零点位于线上，再到梅纳德和古斯（2024）用 decoupling 技术突破零密度估计——都是在传统解析数论的框架内步步为营。每一步都需要数十年的积累。

本文要讨论的，是一种根本不同的进路。它不是解析的，而是计算的。它不是渐近的，而是精确的。它不是试图直接证明黎曼猜想，而是试图将一个等价的计算模型的行为研究到极致。

这种进路的思想史可以追溯到图灵、哥德尔和丘奇的工作。1936 年，图灵在解决希尔伯特判定问题时，创造了图灵机的概念——一种极度简化的计算模型，却能捕捉所有"可计算"的本质。图灵证明了停机问题是不可判定的：不存在一个通用算法能判定任意图灵机是否停机。哥德尔的不完备定理则告诉我们，在任何包含基础算术的公理系统中，都存在既不能被证明也不能被否证的命题。

那么，具体到黎曼猜想：是否存在一台具体的、小型图灵机，其停机行为等价于黎曼猜想的否定？如果存在，它的"大小"是多少？我们能否通过研究这台机器的计算行为，获取关于黎曼猜想的新知识？

这些问题在 2016 年得到了突破性的回答。在本文中，我将：

系统回顾将黎曼猜想编码为图灵机停机问题的理论链条（第 2 节）；
报告该领域的最新进展——744 状态图灵机（第 3 节）；
提出我们的"ZetaHalt"项目，阐述一种不同于穷举搜索的研究范式（第 4 节）；
讨论这一路径对"证明"与"理解"之关系的哲学意义（第 5 节）。

在正式展开之前，我必须做一个诚实声明：本文所述的计算路径，在可预见的未来，几乎不可能"证明"或"否证"黎曼猜想。它所能做的，是提供一种全新的视角、一套可积累的数据资产，以及一个研究数学形式系统之边界的实验场。

这就是我要讲的故事。

2. 理论地基：从黎曼猜想到停机问题

2.1 Davis-Matiyasevich-Putnam-Robinson：希尔伯特第十问题的遗产

要理解如何将黎曼猜想编码为一台图灵机的停机问题，必须先从希尔伯特第十问题说起。

第十问题问的是：是否存在一个通用算法，能判定任意丢番图方程（整系数多项式方程）是否有整数解？1970 年，Yuri Matiyasevich 给出了否定的答案，完成了一项由 Davis、Putnam 和 Robinson 启动的宏大工程。这个结果可以表述为：

每一个递归可枚举集合都是丢番图的。

翻译成计算理论的语言：任何可以被图灵机半判定的集合（即存在一个算法，当输入属于该集合时输出"是"，否则永不停机），都可以编码为一个丢番图方程的可解性条件。

这个定理的一个推论是：每一个Π₁⁰语句（即形如"对所有自然数 n，P(n）成立"的陈述，其中 P 是原始递归谓词）都等价于一台具体图灵机的停机问题。

黎曼猜想恰好就是一个Π₁⁰语句。

2.2 从黎曼猜想到Π₁⁰

黎曼猜想如何表述为一个Π₁⁰语句？这需要几个关键步骤。

首先，黎曼猜想等价于一个关于切比雪夫函数ψ(n）的不等式（Schoenfeld, 1976）：

[ |\psi(n) - n| < \frac{1}{8\pi} \sqrt{n} \ln^2 n \quad \text{对所有 } n > 1 ]

其中 (\psi(n) = \ln \operatorname{lcm}(1, 2, \dots, n))。

Matiyasevich（2020）将这个连续不等式进一步转化为一个纯整数的不等式。他定义了几个整数序列：

(q(n) = \operatorname{lcm}(1, 2, \dots, n))，最小公倍数
(p(n) = \pi(n))，不超过 n 的素数个数
(f_0(n) = 2^{n-1} n!)
(f_3(n) = (2n+3)!! / 5!!)
(d(n)) 通过递推 (d(n+1) = 2n \cdot d(n) - 2(-1)^n f_0(n)) 定义

然后他构造了判别量：

[ r(n) = f_3(n) - p(n)^2 \left(d(n) \lfloor \log_2 q(n) \rfloor - f_0(n)\right) ]

核心定理：黎曼猜想为真，当且仅当对所有 (n \geq 1)，(r(n) > 0)。

这就是一个Π₁⁰语句：它对所有自然数 n 断言一个原始递归谓词(r(n) > 0\）为真。如果存在任何一个反例 n 使得(r(n) \leq 0)，黎曼猜想即被证伪。

2.3 马蒂亚谢维奇的寄存器机

基于上述等价形式，Matiyasevich（2020）进一步将计算(r(n)\）的算法编码为一台拥有 29 个寄存器和 130 条指令的寄存器机。

寄存器机是一种极简计算模型，只有两种指令：

R++：将寄存器 R 加 1，然后继续下一条指令
R-- jump：如果 R>0，将其减 1 并继续下一条；否则跳转到 jump 处的指令

机器从所有寄存器为空开始，对 n=1,2,3,...依次计算 r(n)。一旦发现某个 n 使得(r(n) \leq 0)，机器立即停机。因此：

黎曼猜想为真 ⇔ 该寄存器机永不停机。

这个等价关系是严格的。无需任何近似，无需任何概率假设。它纯粹是形式系统之间的翻译。

3. 竞赛：让机器尽可能小

3.1 Yedidia 和 Aaronson 的突破（2016）

2016 年 5 月，MIT 博士生 Adam Yedidia 和他的导师 Scott Aaronson 发表了一篇引起广泛关注的论文。他们构造了：

一台 4,888 状态的图灵机，停机当且仅当哥德巴赫猜想为假
一台 5,372 状态的图灵机，停机当且仅当黎曼猜想为假
一台 7,918 状态的图灵机 Z，其停机行为在 ZFC（标准集合论）中不可证明（在一致性假设下）

这是人类历史上首次获得这些不可判定性问题的显式状态上界。要知道，虽然哥德尔不完备定理告诉我们"存在"某个程序其行为是 ZFC 不能证明的，但给出这个程序的具体大小，是完全不同量级的成就。

为了构造这些机器，Yedidia 创造了 Laconic 语言——一种专门编译为小型图灵机的高级语言。他们的工作使用了三个关键思想：

Friedman 的"自然"独立命题：逻辑学家 Harvey Friedman 几十年来致力于寻找"自然"的算术命题，这些命题可证明独立于 ZFC。他的工作为编码提供了素材。
"在带处理"：不是直接编译到底层图灵机，而是先编写一个图灵机解释器（约 4000 状态），然后将高级程序写在带上来解释。这避免了乘法开销。
"内省编码"：充分利用每个图灵机状态隐含的 log(n）比特信息，而非用整个状态来表示一个比特。

3.2 疯狂的状态压缩竞赛

Yedidia-Aaronson 的工作触发了激烈的"状态压缩竞赛"。来自全球的程序员和数学家开始用各种技巧缩减这些机器的状态数。

Stefan O'Rear是最活跃的改进者之一。2016 年 5 月底，他报告：

使用他自创的 Not-Quite-Laconic 系统，将黎曼猜想图灵机压缩到1,008 个状态
将与 Aaronson 和 Matiyasevich 联合工作的结果进一步压缩到744 个状态

这是一个惊人的数字。744 个状态。这意味着在单带、双符号的图灵机空间中，最"简单"的一批机器里，就已经潜伏着足以编码黎曼猜想全部复杂性的结构。

作为对比，目前人类确切知道的忙碌海狸数（Busy Beaver number）只有四个：BB(1)=1, BB(2)=6, BB(3)=21, BB(4)=107。BB(5）的下界已经达到 47,176,870，精确值可能永远无法确定。而 744 状态的机器中，已经存在着这样一个命题：它等价于人类数学史上最深奥的未解难题之一。

3.3 忙碌海狸函数：可知与不可知的边界

Yedidia-Aaronson-O'Rear 的工作揭示了一个深刻的哲学事实：可知性的悬崖比大多数人想象的要近得多。

BB(4）是已知的。BB(5）可能可以确定，BB(6）也许永远无法确定。但 BB(744）不仅仅是不确定——确定它的值将等价于解决黎曼猜想。BB(7,918）更甚：确定它的值将等价于解决一个独立于 ZFC 的命题。

这不是一个渐近的、理论上的界线。这是一个精确的、显式的数字。在单带双符号图灵机的序列中，大约在 700-800 个状态之间，数学的"可知区域"开始与"哥德尔区域"重叠。

这对于任何一个关注形式系统之边界的人来说，都是一个令人战栗的事实。

4. ZetaHalt：不求解，而观测

4.1 穷举的局限与观测的可能

面对一台 744 状态的机器，最直接的想法是：运行它，看它是否停机。但这不可行——至少对经典计算而言。

744 状态的图灵机，如果它确实永不停机，那么它将在无限的状态空间中游走。即使它最终会停机，所需要的步数也可能远超宇宙中可用的计算资源。Yedidia 和 Aaronson 提到，他们确实运行了这些机器"大约一天"，但当然没有任何结果。他们甚至讲了一个笑话：一台寻找"存在一个平方数大于等于 5 的反例"的图灵机，用 Laconic 编译后，需要运行一个多小时才找到(3^2=9\）并停机。

在忙碌海狸函数的世界里，"运行它，看它是否停机"不是一个可行的研究策略，除了对极少的状态数之外。

4.2 我们的范式：数据驱动的人机协同

这就是 ZetaHalt 项目的起点。我们不企图在确定型计算中穷举搜索这台机器的状态空间。我们要做的是：

模拟与记录：在有限的 n 范围内（目标：n=10^4 到 10^6，使用对数域稳定化技术处理数值爆炸），运行 Matiyasevich 的 29 寄存器机模拟器，生成精确的状态序列数据。
学习：使用因果 Transformer 模型，在已生成的数据上学习预测寄存器机的下一步状态（具体地，预测 log r(n）的值和 r(n）的符号）。
外推与测试：在分布外（out-of-distribution）的范围测试模型的预测能力。如果模型能够在未见过的 n 区间保持高准确率，说明它学到了某种与 n 无关的不变量结构。
解释：使用注意力热力图、集成梯度和符号回归，从训练好的模型中提取候选数学不变量。例如，模型可能发现某个常数 C 使得： [ \log r \approx \log f_3 - C \log(p^2(m - f_0)) ] 如果 C 的拟合值高度稳定，且 C 恰好等于 1，那模型可能只是重新发现了恒等式。如果 C 稳定在 1.05 左右，那模型可能已经发现了某个新的、更紧的下界。
验证：将符号回归生成的候选猜想注入 Phainarete Project 的 PrimeClaw 系统。Prover 智能体在 Lean 4 中尝试形式化证明。Sentinel 验证每一步推理的正确性。如果证明通过，我们获得新的数学引理；如果失败，失败记录也被存入知识图谱。

4.3 目标是什么？

我们需要诚实：ZetaHalt 项目在 18 个月内证明或证伪黎曼猜想的概率接近于零。

这不是一个"解决黎曼猜想"的计划。这是一个"构建研究黎曼猜想之计算对应物的基础设施"的计划。具体而言，我们的 18 个月目标是：

构建对数域稳定模拟器，生成 n=10^4 以上的高质量状态序列
训练一个在分布内预测准确率>99%的 Transformer 模型
通过可解释性方法提取至少一个候选数学不变量
将所有尝试（包括失败的）记录为结构化数据，公开发布

失败的记录本身就是知识。在数学史上，许多重大突破建立在前人系统排除错误路径的基础上。Lakatos 在《证明与反驳》中强调，数学的进步不仅来自正确的证明，也来自对反例和错误的深刻理解。

ZetaHalt 要成为的，就是这样一个系统：即使无法登顶，也要为后来者绘制详细的地形图，标注哪些路已经走过、哪些悬崖需要避开。

5. 哲学反思：证明、理解与机器的"认知"

5.1 "知道"与"理解"的分离

2026 年 1 月，Google DeepMind 的 Gemini 模型在代数几何领域给出了一个让斯坦福教授评价为"如果是我自己想出来的，我会吹一辈子"的证明。但那个证明的逻辑链对人类来说几乎无法追溯——它是"正确的"，但无人"理解"它为什么是正确的。

这就是第四次数学危机的核心：机器产生了人类无法理解的真理。

将黎曼猜想编码为图灵机，进一步放大了这个问题。假如有人在未来的某一天证明了 BB(744）的值，并且这个值恰好"证明"了黎曼猜想——我们会"理解"这个证明吗？

5.2 形式化验证作为桥梁

我们的回答是：形式化验证。Lean 4 这类交互式定理证明器，其内核是一个确定性的类型检查器，不依赖概率，不依赖直觉，只依赖公理和推理规则。任何通过 Lean 4 验证的证明，无论最初是由人类、AI 还是图灵机生成的，都可以被逐步分解、检视和理解。

这就是为什么 PrimeClaw 系统将"Sentinel"设为唯一不使用概率模型的组件。它必须是刚性的。它必须是不说谎的。

5.3 为什么是 744？

744 这个数字本身就有某种美学意义。

它不大——远小于数学中最小的"不可知"状态数的理论估计（可能在数千万甚至更高）。它也不小——远大于人类目前能够穷举探索的 BB(4)=107。

它恰好落在人类理性之光与哥德尔阴影的交界处。

对于形式科学的研究者来说，这意味着：我们不需要到达无穷，就可以触碰到不可判定性的边界。我们只需要一台 744 状态的图灵机，和足够的勇气去直视它。

6. 邀请

ZetaHalt 是一个完全开源的项目（MIT 许可证）。我们欢迎来自数学、逻辑学、哲学、理论计算机科学的研究者参与。

你可以做的：

帮助验证 Matiyasevich 递归公式的正确性；
用 Lean 4 形式化 29 寄存器机的等价性证明；
设计更好的序列模型来预测状态演化；
或者，只是参与这场对话——关于在可知与不可知的边界，我们作为有限理性存在者，可以做什么。

希尔伯特说："我们必须知道，我们必将知道。"

一个世纪之后，也许我们需要补充的是：

"我们必须知道——我们不知道的东西，比我们曾经认为的，要多得多。但这不妨碍我们继续探求，甚至不妨碍我们享受这种探求本身。"

因为在那条 744 状态的传送带上，每一个冰箱门，都是一次叩门。

而叩门本身，已经是一种回答。

参考文献

[1] Hilbert, D. (1900). Mathematische Probleme. Nachrichten von der Königlichen Gesellschaft der Wissenschaften zu Göttingen, Mathematisch-Physikalische Klasse, 253-297.

[2] Riemann, B. (1859). Ueber die Anzahl der Primzahlen unter einer gegebenen Grösse. Monatsberichte der Berliner Akademie.

[3] Schoenfeld, L. (1976). Sharper bounds for the Chebyshev functions θ(x) and ψ(x). II. Mathematics of Computation, 30(134), 337-360.

[4] Matiyasevich, Y. (2020). The Riemann Hypothesis in computer science. Theoretical Computer Science, 812, 49-65.

[5] Yedidia, A., & Aaronson, S. (2016). A relatively small Turing machine whose behavior is independent of set theory. arXiv:1605.04343.

[6] Matiyasevich, Y., O'Rear, S., & Aaronson, S. (2016). 744-state Turing machine that halts iff there's a counterexample to the Riemann Hypothesis. [Announcement on Shtetl-Optimized, May 30, 2016].

[7] Turing, A. M. (1937). On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 2(1), 230-265.

[8] Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38, 173-198.

[9] Davis, M., Matiyasevich, Y., & Robinson, J. (1976). Hilbert's tenth problem: Diophantine equations: positive aspects of a negative solution. Proceedings of Symposia in Pure Mathematics, 28, 323-378.

[10] Lakatos, I. (1976). Proofs and Refutations: The Logic of Mathematical Discovery. Cambridge University Press.

项目链接

代码仓库：https://github.com/Phaenarete-Project/ZetaHalt
项目主页：https://riemann.phaenarete.org（正在开发）
联系方式：[email protected]