ZetaHalt：当黎曼猜想遇上寄存器机——一个离散等价形式的数学与计算分析

本文面向专业数学与计算机科学工作者，试图以尽量自包含的方式，阐述 Matiyasevich (2020) 将黎曼猜想编码为寄存器机停机问题的深刻构造，并在此基础上讨论 ZetaHalt 项目的实验方法论边界。所有公式均经过与原文的逐式核对；任何遗留的笔误由笔者负责。

一、问题的来龙去脉：为什么一个离散等价形式值得认真对待

黎曼猜想（Riemann Hypothesis, RH）的表述极为简洁：非平凡零点的实部均为 $1/2$ 。然而，这一陈述的推论却极为深远。Hardy (1914) 证明了临界线上存在无穷多个零点；Selberg (1942) 进一步证明了正比例零点定理；近年来，Guth 与 Maynard (2024) 对零点密度估计的改进，以及 de Bruijn–Newman 常数上界的不断收紧，都在以各自的方式逼近这一堡垒。但正如所有研究者深知的那样：我们仍然没有证明它。

在此背景下，一个自然的问题是：如果我们无法直接证明 RH，能否将它等价地转化为另一种形式的问题，使得这一形式更适合某种新的数学工具或计算范式？

这正是 Matiyasevich (2020) 的核心贡献。他证明了一个惊人的事实：黎曼猜想等价于一台具体的寄存器机（register machine）——仅由 29 个寄存器和 130 条极其简单的指令组成——从全零初始状态出发永不停机。

这个等价关系不是哲学层面的隐喻，而是严格的数学定理。寄存器机的指令只有两种：

R++：将寄存器 $R$ 加 1，继续执行下一条指令；
R-- J：若 $R>0$ ，则减 1 并继续执行下一条；否则跳转到指令 $J$ 。

换言之，这台机器的行为是完全确定的。它的停机与否，编码了黎曼猜想的真伪。

这一构造的重要性在于：它将一个关于复分析零点的连续问题，投影到了一个离散的、确定性的、可逐步观测的计算轨迹上。这意味着，原则上，我们可以通过观察这台机器的前 $N$ 步行为，来收集关于 RH 的某种信息——尽管这种信息不能替代证明，但它可能揭示出传统解析方法难以捕捉的结构。

ZetaHalt 项目正是建立在这一认识之上。它不是一个"证明 RH 的项目"，而是一个计算实验室：精确复现 Matiyasevich 的构造，生成可认证的数据，并在此基础上探索机器学习等新工具能为这一古老问题提供何种补充性的结构洞察。

二、从解析数论到整数递推：等价链的完整推导

要理解 Matiyasevich 的构造，我们必须从等价链的起点开始，逐步追溯每一个数学环节。

2.1 切比雪夫函数与 von Koch 等价

定义切比雪夫函数（Chebyshev function）为

\psi(x) = \sum_{p^k \leq x} \log p,

其中求和遍历所有不超过 $x$ 的素数幂。对于正整数 $n$ ，一个基本恒等式是

\psi(n) = \log \operatorname{lcm}(1, 2, \ldots, n).

这是因为 $\operatorname{lcm}(1, \ldots, n)$ 中素数 $p$ 的指数恰好是满足 $p^k \leq n$ 的最大整数 $k$ ，取对数后即为 $\log p$ 的贡献之和。

von Koch (1901) 的经典定理建立了 RH 与 $\psi$ 函数的误差项之间的等价关系：

定理（von Koch, 1901）. 黎曼猜想成立，当且仅当
$\psi(x) = x + O(x^{1/2} \log^2 x).$

这个等价关系的证明依赖于黎曼显式公式：若 RH 成立，则零点项的衰减足够快，使得误差项被控制在 $O(x^{1/2}\log^2 x)$ ；反之，若误差项达到这一阶，则任何偏离临界线的零点都会产生一个过大而无法抵消的振荡项，从而迫使所有非平凡零点位于临界线上。

2.2 Schoenfeld 的显式估计与 Matiyasevich 的单侧界

von Koch 的 $O$ -记号虽然优美，但对于构造具体的计算对象来说不够精确。Schoenfeld (1976) 给出了一个更具体的上界：如果 RH 成立，则对所有 $x \geq 73.2$ ，

|\psi(x) - x| < \frac{1}{8\pi} x^{1/2} (\log x)^2.

注意这个条件的方向：它是 RH 的一个推论，而非等价条件。要从误差估计反推 RH，我们需要的是 Ingham (1932) 等人的结果：如果存在某个常数 $C$ ，使得对所有充分大的 $x$ 有

\psi(x) - x < C x^{1/2} (\log x)^2,

则 RH 必然成立。

Matiyasevich 的巧妙之处在于，他构造了一个单侧上界，使得这个上界同时充当 RH 的必要条件和充分条件。具体而言，他证明了：

必要性：若 RH 成立，则对所有 $n > 1$ （而不仅仅是充分大的 $n$ ），
$\psi(n) - n < \frac{1}{25} n^{1/2} (\log n)^2.$
充分性：若对所有充分大的 $n$ 有 $\psi(n) - n < C n^{1/2} (\log n)^2$ （其中 $C$ 可取 $2/5$ ），则 RH 成立。

这里的关键观察是： $1/25 < 1/(8\pi) \approx 0.0398$ ，因此由 Schoenfeld 的显式估计可以直接推出 Matiyasevich 的必要条件；而 Ingham 的 $\Omega_\pm$ 结果保证了这样的单侧上界足以蕴含 RH。这种"夹逼"结构，使得后续的整数化成为可能。

2.3 整数化的核心困难：如何处理对数

现在我们要把上述不等式转化为一个整数判别式。核心困难在于： $\psi(n)$ 涉及自然对数，而自然对数是一个超越函数，无法直接用整数运算表示。

Matiyasevich 的解决方案分为三步：

第一步：用二进制对数代替自然对数。

定义

l(n) = \lfloor \log_2 q(n) \rfloor = \lfloor \log_2 \operatorname{lcm}(1,\ldots,n) \rfloor.

由于 $0 \leq \log_2 q(n) - l(n) < 1$ ，我们有

\psi(n) = l(n) \cdot \log 2 + \varepsilon_n, \quad 0 \leq \varepsilon_n < \log 2 < 1.

这意味着 $l(n)$ 提供了一个以 $\log 2$ 为单位的 $\psi(n)$ 整数近似。

第二步：用有理数逼近 $\log 2$ 。

定义交错调和部分和

b(n) = \sum_{k=1}^{n-1} \frac{(-1)^{k+1}}{k}.

众所周知， $\lim_{n\to\infty} b(n) = \log 2$ 。Matiyasevich 证明了更精确的估计：对所有 $n \geq 30$ ，

|\log 2 - b(n)| < \frac{3}{5n}.

第三步：构造整数序列 $d(n)$ 。

为了消除 $b(n)$ 中的分母，定义

d(n) = (2n-2)!! \cdot b(n) = (2n-2)!! \sum_{k=1}^{n-1} \frac{(-1)^{k+1}}{k}.

由于 $(2n-2)!! = 2 \cdot 4 \cdot 6 \cdots (2n-2) = 2^{n-1}(n-1)!$ ，可以验证 $d(n)$ 是一个整数。

关键递推： $d(n)$ 满足

d(1) = 0, \quad d(n+1) = 2n \cdot d(n) - 2(-1)^n \cdot (2n-2)!!.

这个递推的推导很简洁：注意到 $b(n+1) = b(n) + (-1)^{n+2}/n$ ，两边乘以 $(2n)!! = 2n \cdot (2n-2)!!$ ，整理即得。

三、判别量的构造与渐近验证

3.1 核心变量的完整定义

为了构造最终的判别式，我们需要引入以下变量：

最小公倍数： $q(n) = \operatorname{lcm}(1, \ldots, n)$ ，满足递推
$q(1) = 1, \quad q(n+1) = (n+1) \cdot q(n) / \gcd(n+1, q(n)).$
素数计数： $\pi(n) = \#\{p \text{ prime} : p \leq n\}$ 。利用上述 gcd 递推，可以证明
$\pi(n) = \pi(n-1) + [\gcd(n, q(n-1)) = 1].$
对 $n > 1$ ， $\gcd(n, q(n-1)) = 1$ 当且仅当 $n$ 是素数（因为任何合数 $n$ 都含有不超过 $n-1$ 的素因子，从而与 $q(n-1)$ 共享该因子）。
二进制对数整数部： $l(n) = \lfloor \log_2 q(n) \rfloor$ 。
整数化乘积： $m(n) = d(n) \cdot l(n)$ 。
双阶乘尺度 1： $f_0(n) = \frac{(2n)!!}{2} = 2^{n-1} n!$ ，递推为 $f_0(n+1) = 2n \cdot f_0(n)$ ，初值 $f_0(1) = 1$ 。
双阶乘尺度 2： $f_3(n) = \frac{(2n+3)!!}{5!!} = \frac{(2n+3)!!}{15}$ ，递推为 $f_3(n+1) = (2n+5) \cdot f_3(n)$ ，初值 $f_3(1) = 1$ 。

3.2 为什么 $m(n) - f_0(n)$ 编码了 $\psi(n) - n$

这是整个构造中最精妙的一步。让我们仔细推导：

首先，由定义：

\frac{d(n)}{f_0(n)} = \frac{(2n-2)!! \cdot b(n)}{2^{n-1} n!} = \frac{2^{n-1}(n-1)! \cdot b(n)}{2^{n-1} n!} = \frac{b(n)}{n}.

由于 $b(n) \to \log 2$ ，我们有

\frac{d(n)}{f_0(n)} \sim \frac{\log 2}{n}.

现在， $m(n) = d(n) \cdot l(n)$ ，而 $l(n) \approx \psi(n) / \log 2$ ，因此

m(n) = f_0(n) \cdot \frac{b(n)}{n} \cdot l(n) \approx f_0(n) \cdot \frac{\log 2}{n} \cdot \frac{\psi(n)}{\log 2} = f_0(n) \cdot \frac{\psi(n)}{n}.

于是

m(n) - f_0(n) \approx f_0(n) \left(\frac{\psi(n)}{n} - 1\right) = \frac{f_0(n)}{n}(\psi(n) - n).

这正是我们想要的效果： $m(n) - f_0(n)$ 的量级被 $f_0(n)/n$ 所缩放，而其相对大小编码了 $\psi(n) - n$ 。

3.3 判别量 $r(n)$ 的构造与渐近一致性

Matiyasevich 的核心不等式是：

\pi(n)^2 \cdot (m(n) - f_0(n)) < f_3(n).

定义整数判别量

r(n) = f_3(n) - \pi(n)^2 \cdot (m(n) - f_0(n)).

定理（Matiyasevich, 2020）. 黎曼猜想成立，当且仅当对所有整数 $n \geq 1$ ， $r(n) > 0$ 。

让我们验证这个不等式的渐近一致性。左边：

\pi(n)^2 \cdot (m(n) - f_0(n)) \sim \left(\frac{n}{\log n}\right)^2 \cdot \frac{f_0(n)}{n} (\psi(n) - n) = \frac{f_0(n) \cdot n}{\log^2 n} (\psi(n) - n).

右边：利用 Stirling 公式，

f_3(n) \sim C_0 \cdot f_0(n) \cdot n^{3/2}.

因此，不等式 $r(n) > 0$ 渐近等价于

\frac{f_0(n) \cdot n}{\log^2 n} (\psi(n) - n) \lesssim f_0(n) \cdot n^{3/2},

即

\psi(n) - n \lesssim n^{1/2} \log^2 n.

这正是 von Koch–Schoenfeld 型的误差界。因此，判别量的构造在渐近意义下是完全自洽的。 $\square$

四、从递推公式到寄存器机

4.1 寄存器机模型

寄存器机（register machine）是一种极简的计算模型，由 Minsky (1961) 和 Lambek (1961) 独立提出。一台寄存器机有有限个寄存器（每个存储一个非负整数）和一个程序计数器。指令只有两种：

L: R++：将寄存器 $R$ 加 1，然后执行下一条指令（地址 $L+1$ ）；
L: R-- J：若 $R > 0$ ，将其减 1 并执行下一条；否则跳转到指令 $J$ （如果 $J=0$ 则停机）。

这个模型是图灵完备的：任何部分递归函数都可以被寄存器机计算。但它的指令极为原始——只有加一和条件减一——这使得它成为衡量计算复杂性的一个自然基准。

4.2 Matiyasevich 的 29 寄存器、130 指令构造

Matiyasevich 将上述所有整数递推编码成了寄存器机程序。这台机器有 29 个寄存器，分别对应：

主寄存器（11 个）： $N$ （对应 $n$ ）， $P$ （对应 $\pi(n)$ ）， $D$ （对应 $d(n)$ ）， $M$ （对应 $m(n)$ ）， $F0$ （对应 $f_0(n)$ ）， $F3$ （对应 $f_3(n)$ ）， $Q$ （对应 $q(n)$ ）， $G$ （对应 gcd 中间值）， $H0$ 和 $H1$ （用于处理 $(-1)^n$ 的符号交替），以及 $S$ （奇偶性标志）。
辅助寄存器（18 个）：用于在破坏性操作中临时保存值的镜像寄存器（如 $Da, Db, F0a, F0b$ 等）。因为寄存器机没有堆栈或额外存储，所有中间值都必须通过寄存器复制来实现。

130 条指令被组织成以下功能块：

初始化（6 条）：设置初值。
测试循环：计算 $m - f_0$ （若结果为负则取 0），并将 $f_3$ 复制到临时寄存器 $F3m$ 。
乘法和比较（约 17 条）：将 $p^2$ 加载到临时寄存器，然后执行 $p^2$ 次循环，每次从 $F3m$ 中减去 $m$ 。如果在此过程中 $F3m$ 归零而循环尚未结束，说明 $p^2 \cdot m > f_3$ ，即 $r(n) \leq 0$ ，机器停机。
欧几里得算法（约 16 条）：计算 $\gcd(n, q(n-1))$ 。
主递推计算（约 34 条）：更新 $d, f_0, f_3, q$ 等变量。
符号处理（约 18 条）：通过 $S$ 寄存器处理 $(-1)^n$ 。
素数更新（约 11 条）：若 $n$ 是素数，则更新 $p$ 和 $p^2$ 。
整数除法（约 11 条）：计算 $q(n) = n \cdot q(n-1) / \gcd$ 。
对数累加（约 12 条）：计算 $l(n) = \lfloor \log_2 q(n) \rfloor$ 并累加 $m = d \cdot l$ 。

关键观察：虽然单个宏步（从 $n$ 到 $n+1$ ）只对应一行数据，但寄存器机需要执行数千条微步指令才能完成。这意味着，严格意义上的"寄存器机模拟"不是生成每行一个状态，而是需要记录每一条微步指令后的完整寄存器配置。

五、ZetaHalt 项目：一个计算实验室的架构

ZetaHalt 项目的目标不是用机器"证明"黎曼猜想，而是建立一个可复现、可认证、可扩展的计算基础设施，用于研究这个离散等价系统。项目的架构分为三个层级：

5.1 精确整数模拟

这是项目的基石。使用 Python 的任意精度整数（int），严格实现 Matiyasevich 图 2 的 Python 程序。

核心代码的逻辑非常清晰（以下用伪代码表示）：

初始化：h0 = m = p = 0; d = f0 = f3 = n = q = 1

循环（当 p^2 * (m - f0) < f3 时）：
    // 更新 d(n+1)
    d = 2*n*d - 4*(-1)^n * h0   // 注意：这里用的是 (2n-2)!! 的倍数形式
    
    n = n + 1
    g = gcd(n, q)
    q = n * q // g
    
    if g == 1:
        p = p + 1
    
    // 计算 l(n) = floor(log_2 q(n))，并累加 m = d * l
    m = 0; g_temp = q
    while g_temp > 1:
        g_temp = g_temp // 2
        m = m + d
    
    h0 = f0
    f0 = 2 * n * h0
    f3 = (2*n + 3) * f3

验证：我们对 $n \leq 1000$ 进行了测试，确认所有 $r(n) > 0$ ，且程序未停机。同时，我们进行了交叉验证：

直接按数学定义计算 $r(n)$ ，与程序逻辑结果比对；
对小 $n$ 用暴力法计算 $\operatorname{lcm}$ 和素数计数，确认 $q(n)$ 和 $\pi(n)$ 的递推正确性；
验证 $d(n) = (2n-2)!! \cdot b(n)$ 与递推结果的一致性。

局限： $f_0(1000)$ 已经是一个超过 $10^{2567}$ 的巨大数字。在普通硬件上，精确整数计算的效率随 $n$ 指数下降。这促使我们转向第二层。

5.2 对数域认证模拟

为了在更大的 $n$ 范围内生成数据，我们采用对数域模拟。核心思想是：不存储 $x$ 本身，而是存储 $\log x$ 。

关键操作：

乘法变加法： $\log(xy) = \log x + \log y$
除法变减法： $\log(x/y) = \log x - \log y$
加法需要特殊处理： $\log(x+y) = \log x + \log(1 + e^{\log y - \log x})$ （假设 $x > y > 0$ ）

认证问题：ZetaHalt 的核心是判断 $r(n) = f_3(n) - \pi(n)^2(m(n) - f_0(n)) > 0$ 。在对数域中，这等价于判断两个极大数 $A = f_3(n)$ 和 $B = \pi(n)^2(m(n) - f_0(n))$ 的差是否为正。当 $A \approx B$ 时，双精度浮点数的精度损失可能导致符号判断错误。

解决方案：

使用多精度浮点（如 mpmath）而非双精度；
为每个计算量维护误差区间 $[x_{\text{low}}, x_{\text{high}}]$ ；
如果区间跨过 0（即 $x_{\text{low}} < 0 < x_{\text{high}}$ ），标记为"不确定"，不用于训练；
对不确定的样本，回退到精确整数计算（如果 $n$ 在精确计算的能力范围内）。

这一策略确保了我们生成的数据集在符号判断上是可认证的，而不仅仅是数值近似的。

5.3 寄存器机微步模拟

这是最深层的实现。我们编写了一个寄存器机解释器，逐条执行 Matiyasevich 的 130 条指令。每一微步都记录了完整的 29 寄存器状态。

验证：对 $n \leq 100$ ，我们验证了微步模拟的聚合结果与高层递推完全一致。这确认了：

130 条指令的翻译是正确的；
寄存器之间的数据流与数学递推一致；
停机条件（ $r(n) \leq 0$ 时跳到指令 0）正确地等价于高层的不等式。

然而，微步模拟的代价极高：每个 $n$ 对应数千条指令。目前我们主要用于验证，而非数据生成。未来的形式化验证工作需要依赖这一层。

六、机器学习：边界、方法与失败标准

6.1 机器学习不能做什么

首先必须明确一个基本原则：机器学习模型不能证明黎曼猜想。

原因有三：

有限数据无法证明全称命题。 无论模型在 $n \leq N$ 上表现多么完美，它不能推断 $n = N+1$ 的情况。RH 是一个 $"\forall n"$ 的命题，不是 $"\exists n"$ 的命题。
全正标签的退化。 如果我们把任务设计为"预测 $r(n)$ 是否大于 0"，由于已观测范围内所有样本都是正的，一个恒输出"正"的模型就能获得 100% 准确率。这不能说明任何问题。
特征泄漏的风险。 如果输入特征包含了 $m(n), f_0(n), f_3(n)$ 等直接参与 $r(n)$ 定义的变量，模型本质上只是在学习代数恒等式，而不是发现新结构。

6.2 机器学习能做什么

在有明确边界的前提下，机器学习可以在以下方面提供补充性的结构洞察：

（一）安全裕度预测

与其预测符号，不如预测安全裕度：

\mu(n) = \log r(n) - \log f_3(n) = \log \frac{r(n)}{f_3(n)}.

$\mu(n)$ 衡量了判别量 $r(n)$ 相对于其主导项 $f_3(n)$ 的"安全边际"。 $\mu(n)$ 越小，系统越接近边界。这个量始终为负（因为 $r(n) < f_3(n)$ ），其变化趋势包含了丰富的信息。

（二）跨尺度外推

真正的测试不是"在训练集上表现好"，而是"在更大尺度上是否仍然遵循相同规律"。我们设计了严格的外推协议：

协议 A：在 $n \leq 1000$ 上训练，测试 $1000 < n \leq 10000$ （近外推）；
协议 B：在 $n \leq 1000$ 上训练，测试 $10000 < n \leq 100000$ （远外推）；
协议 C：按数量级分层（如训练到 $10^3$ ，测试 $10^3$ 到 $10^5$ ）。

如果模型在远外推时性能急剧下降，这是一个有意义的信号：它说明系统在某个尺度上发生了质变，或者模型只是过拟合了训练分布的局部模式。

（三）符号回归与候选不变量

符号回归可以从模型学到的映射中提取候选公式。但这里有一个严格的筛选标准：

代数平凡性检查。 如果一个候选式可以从 $r(n) = f_3(n) - \pi(n)^2(m(n) - f_0(n))$ 直接推出，它不是新发现。
跨尺度数值验证。 候选式必须在训练区间外至少一个数量级上成立。
形式化候选。 通过筛选的式子应被转写为 Lean 4 命题，交由形式化验证系统检验。

例如，符号回归可能发现类似以下的候选式：

\frac{r(n)}{f_3(n)} \approx C \cdot n^{-\alpha} \log^{\beta} n

其中指数 $\alpha$ 和 $\beta$ 可以被与 Schoenfeld 型误差界进行比较。如果模型学到的衰减率与理论预测一致，这强化了我们对构造正确性的信心；如果不一致，则可能提示我们重新审视某些假设。

6.3 实验设计原则

特征集分级：

Lean 集：只给 $n, \log q(n), \log \pi(n)$ 。考察模型能否从最少信息中学习。
Partial 集：给 $\log d, \log f_0, \log f_3, \log l$ ，但不给 $m$ 和 $r$ 。
Full 集：所有变量。仅作为上界或 sanity check。

基线模型：

常数预测器（均值）
线性自回归（AR）
梯度提升树（GBDT）
公式 Oracle（直接用递推计算，理论上界）

评价指标：

MSE 和相对误差
最坏低估比： $\min_n \hat{r}(n)/r(n)$ （若小于 0，说明模型错误预测了符号）
外推退化率
不确定样本比例

七、形式化验证的远景

ZetaHalt 的最终目标之一，是将这一构造嵌入形式化验证系统。具体而言：

寄存器机语义：在 Lean 4 中形式化 Minsky-Lambek 寄存器机的操作语义，验证 130 条指令的正确性。
递推等价性：证明高层递推（ $f_0, f_3, d, q$ 等）与寄存器机执行之间的语义等价。这已在 $n \leq 100$ 的范围内通过计算反射验证。
Matiyasevich 定理的形式化：证明不等式 $r(n) > 0$ 与 RH 的等价性。这需要形式化 Stirling 公式、素数定理的显式误差界、以及 von Koch–Ingham 的等价性证明。
候选不变量的自动验证：将符号回归产生的候选式自动转写为 Lean 命题，由 Prover 智能体尝试证明，Sentinel 负责验证。

这是一个雄心勃勃的长期计划。短期内的可行目标是完成第 1 步和第 2 步，即验证寄存器机的正确执行和递推等价性。

八、失败哲学与开放科学

我必须坦率地说：ZetaHalt 在可见的未来内不会证明黎曼猜想。 这不是谦虚，而是对问题难度的清醒认识。然而，这并不意味着项目没有价值。

正如 Lakatos 在《证明与反驳》中强调的：数学的进步不仅来自正确的证明，也来自对错误路径的系统排除。 ZetaHalt 项目的一个核心承诺是，所有的失败——无论是失败的模型、无法外推的假设、还是被证伪的候选不变量——都将被结构化地记录和公开。这些"死胡同"本身就是知识资产：它们为后续研究者提供了导航图。

失败的标准：

如果模型只是在重新发现定义式，那说明我们的特征集设计有缺陷，需要改进；
如果模型无法跨尺度外推，那说明我们对系统结构的理解还不够深入；
如果候选不变量在数值检验中被证伪，那说明符号回归捕获的是虚假的相关性。

每一次失败，都是对这一古老问题理解的深化。

九、结语

ZetaHalt 项目代表了一种新的研究范式：将最深层的分析数论问题，通过一个精确的、可计算的等价构造，投影到离散的计算轨迹上，然后以开放科学的方式系统地研究这一轨迹。

这个范式有以下几个显著特点：

数学严谨性。 所有构造都经过与原始文献的逐式核对，所有变量都有精确的定义和递推，所有渐近关系都经过一致性检验。
计算可验证性。 从精确整数模拟到对数域认证模拟，从高层递推到寄存器机微步，每一层都有明确的验证协议和交叉检验。
AI 的谦逊定位。 机器学习不是来证明定理的，而是作为探索工具，生成候选假设，辅助人类数学家发现新的结构模式。所有假设都必须经过严格的形式化验证才能被接受。
开放科学。 所有代码、数据、模型和失败记录都是公开的。研究过程本身是透明的，失败本身也是有价值的。

黎曼猜想仍然是人类知识边界上的一道壮丽屏障。ZetaHalt 不声称要跨越这道屏障，但它为我们提供了一架精密的望远镜，让我们得以从全新的角度观察屏障背后的结构。也许，正是这些观察，将为未来的突破铺平道路。

致谢与参考

感谢 Yu. Matiyasevich 教授的奠基性工作，以及 Phaenarete Project 团队的支持。特别感谢审稿人对初稿的深刻批评，这些批评极大地提升了本文的数学严谨性。

Y. Matiyasevich, "The Riemann Hypothesis in computer science," Theoretical Computer Science 807 (2020), 257–265.
H. von Koch, "Sur la distribution des nombres premiers," Acta Mathematica 24 (1901), 159–182.
L. Schoenfeld, "Sharper bounds for the Chebyshev functions $\theta(x)$ and $\psi(x)$ . II," Mathematics of Computation 30 (1976), 337–360.
A. E. Ingham, The Distribution of Prime Numbers, Cambridge Tracts in Mathematics 30, 1932.
M. L. Minsky, "Recursive unsolvability of Post's problem of 'Tag' and other topics in theory of Turing machines," Annals of Mathematics 74 (1961), 437–455.
J. Lambek, "How to program an infinite abacus," Canadian Mathematical Bulletin 4 (1961), 295–302.
I. Lakatos, Proofs and Refutations: The Logic of Mathematical Discovery, Cambridge University Press, 1976.

本文所有数学公式均经过与 Matiyasevich (2020) 原文的逐式核对。任何错误由作者负责。最新版本和完整代码见 https://github.com/Phaenarete-Project/ZetaHalt。