计算机科学家Scott Aaronson为此还写了一篇博文，并大肆赞赏：

　　早在40多年前，一群计算机科学家在德国多特蒙德举行竞赛，寻找“忙碌海狸”图灵机。

　　找出一个特定的图灵机，在它停止之前能够写下最多的1（我们称之为忙碌海狸数）。

　　通过找出特定状态下能在停止前写下最多1的图灵机，我们能更好地理解计算理论的边界。

　　而现在，来自世界各地的20多名贡献者（其中大多数人没有传统的学术资格） ，使用一款名为Coq证明助手的软件获得了结果——47,176,870，该软件证实数学证明没有错误。

　　这一成就瞬间令社区沸腾，其中爱尔兰梅努斯大学计算机科学家Damien Woods惊叹：

　　由一个无限长的纸带，一个读写头（可以读取和写入纸带上的信息），以及一组内部状态等基本部分组成。

　　图灵机的行为由一组规则定义，这些规则可以想象成一张表。表中的每行代表一个规则，每列对应读写头读取到的符号（0或1）。

　　每条规则指定了在特定状态下，读写头遇到0或1时应该执行的操作。操作通常包括：

　　除了处理0和1的规则外半岛彩票，还有一条特殊规则告诉图灵机何时停止运行。当图灵机进入这个状态时，它就不再执行任何操作，相当于“比赛结束”（这种状态一般不计算在状态集合里）。

　　一些图灵机会相对较快地停止（比如这台three-rule图灵机在11步后停止）

　　他还进一步提到，停机问题没有通用的解决方案，因为人们永远无法确定适用于一台机器的方法是否也适用于另一台机器。

　　对于这个结论，数学家Tibor Radó（以下简称拉多）不太满意，并由此发明了“忙碌的海狸游戏”。

　　例如，一组代表所有只有一条规则的图灵机，另一组代表所有有两条规则的图灵机，依此类推。

　　1962年，拉多利用这些有限的图灵机组定义了“忙碌海狸游戏”。游戏的玩法是：

　　3.观察这些机器的运行。一些机器可能会无限期地运行下去，而其他的则会在某个时刻停止。

　　4.在那些最终停止的机器中，有的会很快停止，有的则需要更多步骤。每个组中会有一个运行时间最长的机器，这台机器被称为“忙碌海狸”。

　　5.在有n条规则的组中，这台“忙碌海狸”在停止之前所执行的步数就是所谓的“忙碌海狸数”BB(n)。

　　拉多给这样“极度低效”的图灵机取了一个有趣且形象的名字：忙碌海狸（Busy Beaver，取自英语中的谚语 as busy as a beaver）。

　　Allen Brady（以下简称布雷迪），当时的俄勒冈州立大学数学研究生，成了早期挑战者之一半岛彩票。

　　在游戏推出前，人们已经确定了BB(1) = 1，BB(2) = 6，当时人们正尝试攻克BB(3)。

　　布雷迪也投身BB(3)，他编写了计算机程序来模拟图灵机的行为，这个程序构建了一种“家谱”，根据图灵机初始行为的相似性，对具有相同规则数量的机器进行分类。

　　程序只在机器之间行为差异变得重要时才将家谱树分成多个分支。如果模拟显示某条分支上的机器会停止或进入无限循环，程序就会剪掉这个分支，排除那些不会无限运行下去的图灵机。

　　在1964年，这不是一件容易的事。最终，他在90英里外的灵长类动物研究实验室找到了一台SDS 920计算机。

　　只可惜BB(3)进行到一半，拉多的研究生Shen Lin已宣布证明BB(3) = 21，不过布雷迪还是继续证实了Lin的结果。

　　1966年，他发现了一个在停止前运行了107步的四规则图灵机，并推测这可能是第四个忙碌海狸，并最终于1974年证明了没有其他停止的机器能运行更久。

　　1982年，第一次大规模寻找BB(5)）的Dortmund竞赛正式举办，其中运行时间最长的一台在超过10万步后停止。

　　1984年，《科学美国人》对这项比赛的报道激发了新一代研究者的兴趣，有一位研究者打破了旧纪录，他发现的一台机器在超过200万步后停止。

　　这一新纪录也引来当时的研究生Heiner Marxen和 Jürgen Buntrock，他们在业余时间合作研究这个问题，开发了加速图灵机模拟的数学技术。

　　尽管未能打破200万步的纪录，但后来在1989年，Marxen在一家公司工作时，使用一台功能强大的新计算机重新启动了他的搜索程序，并意外地发现了一个在4700万步后停止的图灵机。

　　经过两年的不懈努力，他开发了一个能够识别非停止机器新种类的计算机程序。尽管他的程序运行了一周并留下了约100个未解决的图灵机，但他手工分析后将名单减少到43个。

　　2022年，研究生Tristan Stérin发起了“忙碌海狸挑战”，这是半岛彩票官方APP下载一项在线合作，旨在最终确定BB(5)。

　　在这之前，Stérin决定在传统方法的基础上进行调整，使用布雷迪的家谱方法，并计划用独立程序处理永远运行的机器。

　　到2021年底，Stérin编写了第一步的计算机程序，生成了大约1.2亿台可能的图灵机列表。

　　为了帮助分析这些机器，Stérin构建了一个在线界面，使用“时空图”来可视化图灵机的行为。

　　完成这些后，鉴于个人精力有限，他在偶然的情况下拉来了Shawn Ligocki半岛彩票。

　　Ligocki向团队介绍了封闭磁带语言方法，这是一种30年前的技术，他将其应用于当前的忙碌海狸问题。

　　他写了一篇博客文章介绍这项技术，但最初并不知道如何编写一个能涵盖所有情况的程序。

　　然后，又一位Justin Blanchard加入了项目，他想出了如何做到这一点，但他的程序相对缓慢。

　　于是另外两个贡献者找到了让它运行得更快的方法，这一技术甚至可以处理前文提到的43个未解决半岛彩票官方APP下载图灵机中的10个。

　　第一个是Skelet #1，它在可预测行为和混乱行为之间不断交替，这种特性使得它非常难以分析和理解。

　　2023年3月，Ligocki和斯洛伐克贡献者Pavel Kropit半岛彩票官方APP下载z（不会说英语，使用谷歌翻译与团队其他成员交流），使用Marxen和Buntrock（之前挑战200万步记录的两位学生）30年前的加速模拟技术的一个增强版，最终破解了Skelet #1。

　　他们发现Skelet #1在超过一万亿步之后才进入一个异常长的重复周期，远超过一般无限循环在1,000步内开始重复的常规。

　　由于Skelet #1的行为极其奇怪，Ligocki在将近五个月的时间里都不确定他们的证明结果是否正确。

　　后来，一位21岁自学成才的程序员（以“mei”为名）加入了团队，她通过学习Coq证明助手，将团队的一些证明翻译成Coq语言，提高了证明的严格性和可靠性。

　　第二个突破是Skelet #17，研究者必须像破译四层加密的秘密消息一样，逐层解析其行为模式，才能证明该机器永远不会停止。

　　尽管研究生Chris Xu和其他社区贡献者做了大量工作，但大多数证明尚未翻译成Coq。

　　直到2023年4月，一位名为mxdys的神秘新贡献者加入，并在短短几周内完成了一个40,000行的Coq证明，证实了BB(5) 的值。

　　mxdys证明第五台忙碌海狸在4700万步后停止，确认了Marxen和Buntrock的发现。

　　BB(5)终于确认了，目前相关研究者正在起草一份学术论文，这将是一个补充mxdys的Coq证明的人类可读版本。

　　mxdys和另一位贡献者Racheline发现了一个六规则的图灵机，其停机问题与著名的数学难题“科拉茨猜想”相似。

　　为了避免让大家头疼，此处不再展开这个猜想，各位看官只需要知道它非常难就行。