超越宇宙极限：第六位海狸数再次突破，无法用常规数学符号表达

选自quantamagazine

作者：Ben Brubaker

机器之心编译

当数字逃离人类的想象力：BB (6) 的故事。

现在给你一串数字，你能猜到一下个是多少吗：1、6、21、107，47176870……

如果你没头绪，不必气馁。因为这些数字并不是随意凑出来的，它们就是所谓的「忙碌海狸数」的前五项。它们构成的数列，与理论计算机科学中最令人头疼的问题之一紧密相关。要想弄清这些数的具体值，是一项堪称不可攀登高峰的挑战。六十多年来，这个难题不仅吸引了顶尖数学家的持续攻坚，还让无数业余爱好者为之痴迷，形成了一种独特的「数学文化圈」。

最近，这条探索之路上又出现了新的突破。忙碌海狸猎人们找到了一个全新的冠军程序，它的运行步数之大，以至于用标准的数学符号体系根本无法完整写出。换句话说，他们已经抵达了超出常规数学所能承载的境地。

在上世纪六七十年代，研究人员先后确定了前四个忙碌海狸数。而那个远远庞大的第五个数 BB (5)，直到去年才被彻底锁定。完成这项壮举的，并不是某个顶尖实验室，而是一支由业余数学爱好者组成的团队，他们通过一个名为「Busy Beaver Challenge」的网络社区，日复一日协作攻关，最终拿下了这一难题。

至于 BB (6)，它的真实大小至今仍是一个谜。我们唯一掌握的，只是一些下界 —— 而这些下界本身就已经大到匪夷所思。2022 年，忙碌海狸猎人们证明：BB (6) 至少大到，即使用普通十进制记号也绝无可能完整写下。哪怕你试图把每一个数字都刻在宇宙中每一粒原子上，还没来得及写出有意义的部分，原子就已经耗尽。

「已经远远超出了人类可以想象或真正掌握的范围。」德克萨斯大学奥斯汀分校的计算机科学家 Scott Aaronson 如此感叹。

现在，忙碌海狸猎人们再次刷新纪录：那个已经大到令人难以想象的数字，其实还要更大。最新突破来自 Busy Beaver Challenge 中一位既神秘又高产的贡献者。今年 6 月，他首次为 BB (6) 推出了一个全新的下界；然而仅仅九天之后，他又把纪录再度推高。相比之下，2022 年的下界，如今显得几乎不值一提。

「我一次次被震撼到。」马里兰大学的计算机科学家 William Gasarch 感叹道，「BB (6) 已经把我们带进了庞大数字的『平流层』。」

忙碌海狸真正难题

忙碌海狸背后真正让大家棘手的问题是，给定一段计算机程序的代码，你能判断它最终会停止运行还是会一直运行下去吗？

1936 年，传奇逻辑学家阿兰・图灵就泼过冷水 —— 他证明了，这事儿根本没法儿靠一个万能公式解决。这就是后来赫赫有名的「停机问题」。换句话说，不管你多聪明，哪怕你能搞定一部分程序，必然会有另一些程序让你彻底抓狂。甚至在某些情况下，不存在任何办法可以给出答案。

图灵为了证明这一划时代的结论，创造了一种形式化的数学计算模型。在这个模型里，程序不再是抽象的符号，而被想象成一种理想化的装置 —— 今天我们称之为图灵机。

每一台图灵机都依据一份独特的「规则清单」，一步步地执行计算。规则看似简单，但数量越多，机器的行为就会变得越复杂，也就越难判断它究竟会不会停下来。

但问题是：到底会有多难呢？

1962 年，数学家 Tibor Radó 发明了一种全新的方法来探索这个疑问，他把它称作忙碌海狸游戏。玩法是这样的：先挑一个规则数量 —— 记作 n。你的目标，就是找到那台拥有 n 条规则的图灵机，它能在最终停机之前跑得最久。这台机器就叫忙碌海狸，而它所坚持的步数，就定义为忙碌海狸数 BB (n)。

原则上，如果你想找出任意给定 n 的忙碌海狸，步骤也不算复杂：

列清单：把所有可能的 n 规则图灵机都罗列出来；
做模拟：用计算机程序去运行这些机器；
筛掉「永动机」：很多机器会陷入无限循环，这些明显不会停机的统统剔除；
统计步数：记录剩下的每台机器在停机前走了多少步。

最后，跑得最久、坚持到最后一刻才停下的，就是你的忙碌海狸。

不过，这些步骤在实际操作中，这件事会变得非常棘手。首先，随着规则数量的增加，可能的机器数量会迅速膨胀。要逐一分析它们几乎是一件不可能的事情，因此必须写专门的计算机程序来分类并剔除机器。部分机器很容易判断：要么很快停机，要么陷入一眼就能识别的无限循环。但另一些机器却能运行很久，却丝毫没有显现出明显的规律。正是这种情况，让停机问题赢得了令人望而生畏的声名。

规则加得越多，你就需要越强大的计算力。但仅靠蛮力远远不够。有些机器在最终停机前，会运行得漫长得不可想象，逐步模拟根本不现实。这时，就必须祭出一些精巧的数学技巧，才能测量它们的运行时长。

「技术的进步当然有帮助，」软件工程师、长期的忙碌海狸猎人 Shawn Ligocki 说道，「但帮助也仅限于此。」

一个时代的终结

在 20 世纪 90 年代到 21 世纪初，忙碌海狸猎人们逐渐把注意力转向 BB (6) —— 因为在 BB (5) 的探索中，他们一度陷入僵局。活跃在这股浪潮中的，有 Shawn Ligocki 和他的父亲 Terry，一位应用数学家。父子俩利用劳伦斯伯克利国家实验室的高性能计算机，在闲置时段偷偷运行自己的搜索程序，继续追逐这场数字极限挑战。

终于在 2007 年，他们发现了一台刷新纪录的六规则图灵机。它在停机前足足跑出了近 3,000 位数字的步数。按常理来看，这已经是一个庞大得惊人的数字。然而，它依旧算不上「无法书写」。如果用 12 号字体排版打印，那看似无边无际的三千位数，其实只够铺满一张普通的打印纸 —— 一张薄薄的纸片，竟承载了人类当时所能触及的最大极限。

2022 年，Shawn Ligocki 发现了一台六规则图灵机，它在停机前的运行步数所包含的数字位数，竟然比整个宇宙中的原子数量还要多。

三年后，斯洛伐克一名计算机科学本科生 Pavel Kropitz 决定把攻克 BB (6) 当作自己的毕业论文课题。他编写了自己的搜索程序，并在大学实验室的 30 台计算机上后台运行。一个月后，他发现了一台运行时间远超 Ligocki 父子发现的图灵机 —— 在忙碌海狸猎人的术语中，这就是新的冠军。

「我算是运气好，因为实验室的人已经开始抱怨我占用 CPU 过多，所以我不得不稍微收敛一些。」Kropitz 在 Busy Beaver Challenge 的 Discord 服务器上通过私信写道。又过了一个月，他打破了自己的纪录，找到了一台运行时间超过 30000 位数字的图灵机 —— 足以写满大约 10 页纸。

这台由 Kropitz 找到的机器，保持了 BB (6) 的纪录整整 12 年。

2022 年 5 月，Shawn Ligocki 入职新工作，手里有了强大的计算集群。他心血来潮，把多年前写的老代码搬到新硬件上试跑。果然，他找到了一台新的冠军图灵机，打破了 Kropitz 的纪录。这一发现立刻点燃了忙碌海狸社区的热情。短短两周内，Ligocki 就在邮件列表上两度宣布新的冠军。然而每一次，Kropitz 都能在三天内刷新他的成绩。Ligocki 记得父亲当时惊叹不已。

「他开玩笑说，感觉 Pavel 早就把 BB (6) 解出来了，」Ligocki 回忆道，「因为每当我们宣布一个新冠军，他就会像变魔术一样，从口袋里掏出一个更大的。」

不过，Ligocki 和 Kropitz 后来发现的那两台机器，已经不是多跑一点点，而是把运行时间推向了全新的层级。

要理解这种巨大的数字，我们得回到熟悉的数学操作。

加法：把一个数加 n 次，就是乘以 n。
乘法：把一个数乘 n 次，就是指数运算。

那么，如果我们不断对一个数做指数运算呢？这就定义了一种新的运算，叫做超乘（tetration），用两个向上的箭头↑↑表示。

超乘的增长速度快得惊人：

10↑↑1 只是 10；
10↑↑2 是 10 的 10 次方，即 100 亿；
10↑↑3 是 10 的 100 亿次方，也就是一个 1 后面跟着 100 亿个零。要把所有数字写下来，需要一摞足有 300 米高的纸。
当来到 10↑↑4 时，情况彻底失控：这个数的位数已经远远超过整个宇宙的原子数。

当 Ligocki 第二次超越 Kropitz 时，他找到了一台六规则图灵机，在停机前竟然跑了超过 10↑↑5 步。很快，Kropitz 就以更惊人的成果回应：一台能运行 10↑↑15 步的机器 —— 相当于一座高达 15 层的 10 的幂塔。到此为止，他们已经彻底告别了人类习惯理解的数字世界。

「那是一个时代的终结。」 Kropitz 在私信中写道。

这种终结不止体现在数字的飞跃上，也体现在研究方式的转变上。在此之前，忙碌海狸游戏更像是一场你追我赶的竞技场，研究者们大多单打独斗。而随着 Busy Beaver Challenge 的建立，这场探索进入了一个全新的阶段 —— 从孤军奋战走向开放协作，一个真正的群体探索时代就此开启。

开启新时代的挑战

Busy Beaver Challenge 社区成立于 2022 年，由计算机科学研究生 Tristan Stérin 受 Aaronson 论文的启发而发起。目标十分明确：要严格证明 BB (5) 的真实值。

仅在社区成立两年后，该社区就完成了对 BB (5) 真实值的证明。这个证明过程中深度使用了 Coq 智能证明助手。Coq 通过 Gallina 编程语言，让用户定义数学对象、陈述定理，并一步步构建证明。用户可以与 Coq 进行交互，逐步验证每一步的正确性。Coq 还提供了多种自动化工具，帮助简化证明过程。

2024 年 5 月 10 日，「忙碌的海狸挑战」社区中一位神秘的成员发了一条消息，称「BB (5) 的 Coq 证明已完成。」，他只留下了化名 mxdys。