在数学领域中，存在着一种引人入胜的挑战，那就是寻找忙碌的海狸——这是一类特殊的图灵机，它们在有限步数内尽可能多地写入“1”。这不仅是一项智力游戏，更关乎计算的本质。
斯科特·阿伦森（Scott Aaronson）是研究该领域的专家之一，他指出，早在1983年，图灵机的忙碌海狸问题就已经成为理论计算机科学中最令人着迷的难题之一。他强调，对于那些对数学、计算机的极限以及证明论领域感兴趣的人来说，这是一个理想的研究课题。
忙碌的海狸游戏涉及寻找拥有特定状态数的二进制图灵机，这些机器在停止前能够写入最多的“1”。其中，状态数为“1”的机器已经被彻底解决。一个状态的图灵机是一种具有简单指令集的计算模型，它可以在由0和1组成的无限长的纸带上移动和写入。
早在1974年，两位计算机科学家就提出了寻找这种机器的挑战，他们试图找到拥有两个状态并在停止前能产生最大数量“1”的图灵机。如今，经过近20年的努力，全球的研究者们已经发现了BB(5)的最佳解，其数值分别为47、176和870。
然而，找到这些结果并非易事，Damien Woods表示，这是一项需要极高计算技巧的挑战。该领域的一个难点在于，判定一个给定的图灵机最终是否会停止运行与解决忙碌海狸问题密切相关，而这本身就是一个无法判定的问题。
忙碌海狸问题的核心在于确定哪些图灵机能够最终停止运行。对于任意给定的初始状态，有些机器运行一段时间后便会停止，并在纸带上留下一定数量的“1”。关键的挑战在于确定某个程序是否会最终停止并产生一个确定的输出。
尽管这种不确定性带来了挑战，但它也恰恰是图灵机理论中最核心的概念。图灵机是由艾伦·图灵提出的一个概念模型，用于研究算法的可计算性。
在过去，艾伦·布拉迪等人曾致力于寻找更复杂的图灵机的忙碌海狸，但由于计算量的限制而未能取得突破。他们对该问题的热情和贡献为后来的研究者们奠定了基础。
直到2022年，Tristan Stérin解决了“忙碌海狸五号”问题，这一突破是理论计算机科学领域的一项重要进展，尤其是在确定BB(5)的精确数值方面。该成果的取得离不开计算机辅助证明工具Coq的运用。
尽管这是一个令人瞩目的成就，但要理解其难度，需要认识到计算机科学中存在一些固有的局限性。BB(5)的确定，证明了Coq在应对复杂数学问题上的潜力。与此同时，研究人员也对未来的BB(6)解决方案充满期待。
原文链接：https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/
