选自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。
消息链接:https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237Coq 证明链接：https://github.com/ccz181078/Coq-BB5
当时在弗吉尼亚理工大学读本科的计算机科学学生 Katelyn Doucette 正好读到 BB (5) 被证明的消息，很快被吸引。
「我就这么被迷住了。」她说，「这真是一组无比优美的问题。」
自从完成 BB (5) 的证明后，神秘的 mxdys 就不断向 BB (6) 发起挑战。他采用复杂的自动化方法，将几乎所有候选图灵机分类处理，只剩下几千台待定的图灵机。
Katelyn Doucette 正在翻阅这些待定的图灵机时，注意到其中一台看起来很有潜力，深入分析后发现，这台机器的运行时间仅次于现任冠军。
更令人惊讶的是，这台机器属于一种被称为「移位溢出计数器（shift overflow counters）」的类别，它的长时间运行机制与冠军机完全不同。
「看到这些忙碌海狸机居然找到了『新技术』，真是令人兴奋。」Ligocki 评价道。
既然这类新技术的相关图灵机的最开始的几个样本就能做到与现任冠军接近，那么在后续迭代中，采用移位溢出计数器的图灵机中很可能出现打破记录的新冠军。
于是，Busy Beaver Challenge 的贡献者们立刻涌向其他移位溢出计数器的分析，而 mxdys 又一次抢先一步。
6 月 16 日，他宣布发现了新的冠军：一台能运行 10↑↑107 步的图灵机。
这样的数字，根本不可能写成完整的十进制数列。甚至把它写成幂塔表达式也很奢侈—— 如果用 12 号字体把那一长串的 10↑↑↑↑… 排出来，整条公式能拉长约 40 公里。
正在度假的 Kropitz 看到了消息，他大方地接受了冠军易主的事实，还在 Discord 上调侃道：「很遗憾，这次我没法再来一次三天逆袭了。」
突破全新量级
但这个庞大的「新纪录」仅仅只维持了一周，神秘的 mxdys 大神又一次刷新了自己的纪录，带来了一台运行时间达到全新量级的图灵机。
如果说上一个记录勉强还能使用「超乘」作为数学符号来表达，那这个全新量级的新纪录甚至必须再次引入一个全新的数学符号：五乘（pentation）。
五乘采用三个向上的箭头「↑↑↑」表示，本质上就是「重复做超乘」。
这台冠军机在停机前执行的总步数，大于：2↑↑↑5
也就是：2↑↑(2↑↑(2↑↑(2↑↑2)))。
如果从最里面开始计算：
2↑↑2 = 42↑↑4 = 稍大于 65,000
这样，外层就变成：2↑↑65,000 … 最终结果是一个大到完全超出想象的数，即便用最简洁的符号表达，这个数字依然大到超出了宇宙极限。
就像 BB (5) 在 2024 年才被严格证明一样，BB (6) 的数值远没有达到能被证明的程度。这一超越极限的新纪录仍然只是 BB (6) 的下界 —— 真实值可能还要更高，忙碌海狸猎人们也确实无法能在短期内得到最终答案。
一台被命名为「Antihydra（反九头蛇）」的六状态图灵机给忙碌海狸猎人们带来了很大的麻烦。
研究者几乎可以肯定：「反九头蛇」永远不会停机。但问题是，他们至今没法证明这一点。原因也很清楚：一位代号 Racheline 的猎人展示过，判断反九头蛇是否停机，其实和数学中一个著名的未解难题「考拉兹猜想（Collatz conjecture）」密切相关。
从那以后，团队又发现了许多具有类似特征的六状态机器。
但是，如果要彻底解决同类的六状态机的证明问题，可能需要在纯数学领域取得根本性突破。
不过，对狂热的忙碌海狸猎人来说，这一点都不是沮丧的理由。还有成千上万台六状态图灵机等待探索，每一台都有自己独特而精彩的行为模式。
「对我来说，做数学最正当的理由就是：它好玩。它是一门艺术。」Racheline 在 Discord 的私信里写道，「总会有新的东西值得去探索。」
忙碌海狸问题，和停机问题一样，都是不可计算问题的具体体现，没有一个通用算法能算出所有 BB (n) 的精确值。对于这类问题的探索，能够不断推动计算理论和数学边界的拓展，这也塑造了数学与计算机科学的独特魅力。
参考链接：
https://www.quantamagazine.org/busy-beaver-hunters-reach-numbers-that-overwhelm-ordinary-math-20250822/
https://bbchallenge.org/1RB1RA_1RC1LB_0LD0RA_1LA0LE_0LF1LD_---0LB
https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237
钱程策略配资提示：文章来自网络，不代表本站观点。
