计算机程序在停止之前，能够运行多久？一年，十年，百年，千年，还是宇宙的年龄？如果你不知道答案，你并不孤单。这个问题困扰并迷惑了数学家们超过60年。为什么？它与一些数学最古老、最著名的未解问题有着令人惊讶的联系。它提供了一个窗口，揭示了数学基础逻辑开始崩溃的地方，甚至可能揭示出人类知识的边界。

就在去年，经过30年的无进展，终于取得了一项重大突破，但这项发现真正值得注意的地方，不仅仅是结果，更是它发生的奇怪方式。它并不像大多数数学问题那样被解决，不是由一群在大学里受过高度训练的研究人员来解决的。而是由一群不太可能的数学爱好者解决的，他们大多没有正式的学术教育，他们通过一个名为“忙碌海狸挑战”的网站在线聚集在一起。

这一切始于一位数学家和他发明的一个游戏。当大多数人都在问，“计算机能解决哪些问题？”时，
有位数学家名叫Tibor Rado问道：“计算机无法解决哪些问题？”一个算法，一个按步骤执行的无意识指令集，能真正走多远？所有问题都能计算吗？还是有些问题对于计算机来说太复杂无法处理？计算的极限在哪里？

当时，计算机能解决什么问题是非常清楚的，多亏了艾伦·图灵。他想出了这些简单的理论设备，叫做图灵机，它们正好捕捉到计算的真正含义。

图灵曾假设，这些简单的计算机能够执行任何可能的计算。它们是我们所有现代数字计算机的蓝图，Rado确实找到了一些计算机无法解决的问题，要理解它，我们需要了解图灵机是如何工作的。

图灵机由一条无限长的带子组成，带子被分成若干单元格。每个单元格中都有一个符号，比如零或一。一个“头”读取符号，根据符号的不同，它可以擦除符号，写入新符号，向左移动或向右移动。每个图灵机都有一组独特的规则，这些规则告诉它应该做什么。

例如，第一条规则可能是：“如果读取到零，就在当前单元格写一个一，然后向右移动一个单元格，并转到第二条规则。”

还有一条特殊规则，告诉机器何时停止运行。图灵机可以有任意固定数量的规则。有些有三条规则，有些有10条规则，有些有100条规则。通常，图灵机规则越多，它能做的计算就越复杂。

从第一条规则开始，图灵机最终要么停机，要么一直运行下去。所以图灵机有两种类型，停机型和非停机型。Rado将图灵机按规则数量进行了分类。他将所有1条规则的机器归为一组，所有2条规则的机器归为一组，所有3条规则的机器归为一组，以此类推。

在每组中，有些机器会永远运行下去，有些会很快停机，有些则会花费更长时间才能停机。其中一台机器会是最后停机的。这就是Rado感兴趣的机器，所有停机机器中运行时间最长的。Rado称它们为忙碌的海狸，因为它们在带子上游走。

忙碌海狸在停机之前执行的步骤数称为它的忙碌海狸数，简称BBn。例如，对于1条规则的图灵机，如果你想确保它停机，你实际上只能有一条规则：无论它读取到什么，都让它停机。因此，1条规则图灵机的忙碌海狸数就是1，因为它只需一步就停机。

获取BB2稍微复杂一些，因为有6,561种2条规则的机器，但已证明，忙碌海狸数2的机器运行6步后就停机。现在，重要的部分来了。Rado发现，找出忙碌海狸及其忙碌海狸数是不可计算的。没有通用的算法或公式，计算机无法用来找到它们。找到一个忙碌海狸的唯一方法是逐个检查每台机器，看看它们运行多长时间。

他找到了自己想要的东西。Rado把他寻找忙碌海狸的过程变成了一个游戏。玩这个游戏，你必须做两件事，丢弃所有非停机的机器，然后在剩下的机器中，寻找运行时间最长的那台。他没想到的是，这个游戏竟然与一些数学上最著名的未解问题有关，并且成为了一个跨越几十年的追寻，困扰了几代数学家。

但忙碌海狸与这些著名问题有什么关系呢？为了理解这一点，我们来看其中的一个问题。

哥德巴赫猜想

哥德巴赫猜想说，每个大于二的偶数都可以表示为两个质数的和。例如，4是2和2的和，都是质数。28是17和11的和，都是质数。你对任何偶数这样做都行。这个看似简单的猜想已经无法证明近300年，但到目前为止，我们知道它对于所有小于 4×10¹⁸的偶数成立。

但是，逐个检查每个偶数并不够，数学家们需要一个严谨的逻辑证明，证明它对所有偶数都成立。这时候，一个忙碌海狸可能派上用场了。假设你写了一个计算机程序，从4开始，逐个检查每个偶数，只有在发现一个不能表示为两个质数和的偶数时才停机。

已证明，这个程序对于27条规则的图灵机来说是可计算的。但这里有个有趣的部分。如果我们知道BB27的值，我们就能解决哥德巴赫猜想。如果我们的程序停机，那么它必定在BB27步内停机。如果它在这个步数内停机，那么程序就发现了一个不能表示为两个质数和的偶数。这将证明哥德巴赫猜想是错的。

但如果机器运行超过BB27步，那么我们就知道它永远不会停机，因为所有停机机器都在BB27步之前停机。这将证明哥德巴赫猜想是对的。因此，哥德巴赫猜想的解决方法可以归结为寻找27条规则的忙碌海狸。

还有其他类似的图灵机，它们可以用来解决数学中的其他未解问题，比如黎曼假设。事实上，任何可以用计算机语言写出的数学命题都可以通过这种方式证明。令人惊讶的是，做这件事所需要的有限步骤，竟然能告诉我们无穷多的数字的信息。

那么我们在等什么呢？为什么不去找出BB27，然后解决哥德巴赫猜想，以及所有其他未解的数学问题呢？

为什么寻找忙碌海狸如此困难我们已经看过1条和2条规则的忙碌海狸，但3条规则呢？嗯，3条规则的图灵机超过500万个，而4条规则的图灵机有超过70亿个。记住，找一个忙碌海狸的唯一方法就是逐个检查每台机器。

这就像在一个巨大的数字干草堆中找一根针，而干草堆的大小随着规则数量的增加而呈指数级增长。但我们可以通过去掉所有非停机的机器，然后只检查剩下的机器，让生活变得更轻松吗？非停机的机器显然不是忙碌海狸，因为根据定义，忙碌海狸必须停机。

但图灵给我们带来了一个麻烦的惊喜。他证明了，没有一种可靠的、可重复的方法可以判断图灵机是否会停机。如果一台机器已经运行了100年，它可能会在101年停机，而我们无法判断，除非等着看它会不会停机。这个结果叫做“停机问题”，我做了一个关于它的完整视频，链接在描述中。这是一个非常酷的结果，尽管它有点麻烦。

所以，看来Rado游戏的两步都极其困难，第一步是因为停机问题，第二步是因为要搜索的机器实在太多了。但我们至少找到了第三个忙碌海狸吗？

在1960年代中期，一位坚韧不拔的数学研究生，在俄勒冈州立大学，他的吉祥物碰巧是“本尼海狸”，开始了他的尝试。他叫Allen Brady，他意识到，如果他忽略掉大部分机器，例如那些立即停机的机器，他就可以浏览完所有500万个3条规则的图灵机。

他还认识到，许多非停机的机器很容易辨别，因为它们开始循环，重复执行相同的指令。Brady编写了这个方法，将显而易见的非忙碌海狸丢掉，并将其做成了一个计算机程序，但当时的计算机无法处理如此繁重的计算。Brady不得不寻找先进计算机。

但是，Rado和他的研究生Shen Lin已经抢先一步，他们找到了第三个忙碌海狸。它在21步内停机。但Brady没有放弃希望。他立即开始寻找第四个忙碌海狸。

BB(4)但是有一个问题。四条规则的图灵机比三条规则的图灵机能做更复杂的计算。这意味着它们的非停机机器更难以辨认，因为很多非停机机器并不会陷入无限循环，而Brady的程序正好擅长识别这些循环。

然而，尽管如此，两年后，他还是找到了一台在107步内停机的四条规则图灵机。他花费了更多的岁月，艰苦地工作，终于证明这台机器确实是第四个忙碌海狸。

这时，来到了2024年4月，忙碌海狸挑战赛，一群数学爱好者们的到来。尽管有近17万亿个五条规则的图灵机，他们竟然做到了别人无法做到的事。他们找到了第五个忙碌海狸，即BB5。

大约在Brady找到了第四个忙碌海狸20年后，多特蒙德大学举办了一场比赛，旨在寻找第五个忙碌海狸。超过100位参赛者参加了这场比赛，但比赛结束时，没人能够确定性地找出BB5。

然而，一位参赛者找到了一个在10万步内停机的机器。这场比赛在《科学美国人》上得到了报道，这也使得这项游戏吸引了新一代数学家的关注，不久之后，这个步数很快突破了200万步，并把可能的BB5步数推高了。

但所有人都震惊了，当研究生Heiner Marxen和Jurgen Buntrock发现了一个五条规则的机器，它在47,176,870步内停机。这是不是第五个忙碌海狸？他们当时不知道，直到30年后才有答案。

几十年间进展缓慢，但事情在2021年迎来了突破。一位名叫Tristan Sterin的研究生尝试了Brady的原始方法，只是稍作改动。像Brady一样，Sterin写了一个代码，筛选掉明显不是第五个忙碌海狸的机器。

他把剩余的机器全部收集到一个数据库里，准备进一步检查。到了2021年12月，数据库完成，里面有超过8800万台机器，8800万台可能的忙碌海狸。如果他能证明这些机器中的每一台要么在47百万步之前停机，要么永远不停机，那么他就知道这台47百万步的机器真的就是第五个忙碌海狸。

但他该如何从8800万台机器中筛选出来呢？

Sterin知道他需要帮助，于是他成立了“忙碌海狸挑战”，一个任何人都可以加入的在线社区。来自世界各地的约20人开始共同解决这个问题，而且他们大多数人都没有任何正式的数学训练，他们只是把数学当作兴趣或爱好。

大家开始一点点地剖析这8800万台机器，并通过Discord保持进展更新。

但问题是，有些机器几乎不可能分类。其中有一台机器，声名远播，被大家称为“骨架#1”。这台机器的棘手之处在于，它有时表现得完全可预测，有时却完全不可预测。无法知道它接下来会做什么。

但是经过几个月的反复碰壁，两位贡献者最终成功破解了它。Shawn Ligocki和Pavel Kropitz证明了“骨架#1”最终会陷入一个无限循环，但它需要超过万亿万亿步。终于，他们成功地将它归类为非停机机器，并把它从可能的忙碌海狸列表中剔除。

然而，大家心中仍然存有疑虑。他们能相信他们写的代码吗？即使他们找到了BB5，程序中的任何小错误都可能让他们的结果毫无价值。他们需要证明代码没有任何错误。

但是，如何证明数千行代码没有错误呢？

正是在这个关键时刻，一个新的、不太可能的角色加入了，那就是一个证明检查器。证明检查器是程序，如果遇到逻辑错误，它不会运行，因此几乎不可能有错误。一个好的证明检查器程序，能够毫无疑问地确认，团队的证明没有任何错误的逻辑。

一位雄心勃勃的大学辍学生，自学成才的程序员mei加入了团队。mei把“骨架#1”的证明转化为一种叫做COQ的证明检查语言，验证了Ligocki和Kropitz的结果，证明“骨架#1”永远不会停机。

一点一点地，这座大山开始减小，来自其他参与者的非忙碌海狸证明也逐渐到位，但很多证明仍然没有转化为COQ，以确保它们是合法的、没有错误的。

然后，在2024年5月10日，一位神秘的参与者名为mxdys宣布：“BB5的COQ证明完成了。”他们把整个团队的工作汇集成了一份40,000行的COQ证明。这是忙碌海狸5任务的最后一步。这个来自世界各地的、不太可能的团队，他们因为对数学的热爱聚集在一起，终于证明了这台47百万步的图灵机就是第五个忙碌海狸。

这是一个重大的成就，但不幸的是，并不是每个人都能一起庆祝。第四个忙碌海狸的发现者Allen Brady，在证明完成前几周去世了。他享年90岁。虽然他没能亲眼见证这个里程碑，但他的遗产将永远与忙碌海狸的故事交织在一起。

那么，接下来呢？BB(6)？

爆炸性增长

BB(6)的寻找过程充满了技术挑战和不断的记录突破。2022年，肖恩·利戈基（Shawn Ligocki）发现了一台六规则图灵机，其运行时间超过了宇宙中原子的数量，这一发现引起了极大的关注。三年后，来自斯洛伐克的计算机科学本科生帕维尔·克罗皮茨（Pavel Kropitz）将BB(6)的搜索作为他的毕业论文项目，开始了自己的探索。

克罗皮茨编写了搜索程序，并将其运行在大学实验室的30台计算机上。在一个月的时间里，他发现了一台新的机器，其运行时间远超利戈基的记录，这台机器被称为新的“冠军”。经过进一步的搜索，他又发现了运行时间超过30,000位数字的机器，这足以填满大约10页的纸。这一记录保持了12年，直到2022年5月，利戈基开始了一项新工作，获得了更强大的计算机集群支持，并利用这些资源重新启动了搜索。通过更新的硬件，利戈基很快发现了一台新机器，打破了克罗皮茨的记录。

随着利戈基和克罗皮茨不断刷新记录，两人之间的竞争也变得更加激烈。利戈基和克罗皮茨发现的机器不仅仅比现有的记录稍微更长，而是达到了一个全新的数字层次。为了理解这些数字的规模，我们需要使用“超指数运算”，这是一种增长非常迅速的数学操作。例如，10 ↑↑ 3 表示

• 10 ↑↑ 1 = 10
• 10 ↑↑ 2 = 10^10 = 10,000,000,000（即 10 的 10 次方）
• 10 ↑↑ 3 = 10^10^10（即 10 的 100 亿次方）

当利戈基第二次打破记录时，他的机器运行了超过 10 ↑↑ 5 步，克罗皮茨回应以一台运行了 10 ↑↑ 15 步的机器，创造了一个更高的记录。此时，数字的规模已经超出了我们传统的数学表示方式。

在此后的几个月里，“忙碌海狸挑战”变成了一个合作项目，更多的数学家和计算机科学家加入进来，开始共享数据和计算资源。最终，mxdys，这个神秘的成员，提出了一个新的 BB(6) 下限，采用了更加复杂的自动化分类方法，分析了成千上万台图灵机。

2024年6月，mxdys发现了一个新的冠军，它在停机前运行了 10 ↑↑ 10^7 步——这个数字的大小无法用常规数字表示，而是需要使用更复杂的数学符号。尽管克罗皮茨在消息发布时表示接受失去冠军头衔，但他也继续保持在排行榜上，拥有其他记录。

最终，mxdys通过进一步的突破，提出了一个比此前更为巨大的记录，使用了“超乘法”（pentation），一种更高级的运算方法，来表示这一结果。这些数字已经变得如此庞大，传统的数字书写方法已不再适用，甚至使用幂塔来表示也无法满足其需求。