第五只忙碌的海狸：研究人员逼近计算极限

本文讲述了计算机科学家们如何利用软件程序，经过几十年的努力，最终确定了第五个忙碌的海狸数BB(5)的值为47,176,870。忙碌的海狸问题是指寻找在给定规则数量的图灵机中，运行步数最多的机器，它与计算机科学中的停机问题密切相关。文章详细介绍了从上世纪60年代开始，Allen Brady、Shen Lin、Heiner Marxen、Jürgen Buntrock、Georgi Ivanov Georgiev等研究人员对忙碌的海狸问题的研究历程，以及最终由Tristan Stérin发起的“忙碌的海狸挑战”项目如何汇集众人之力，利用Coq证明助手验证了BB(5)的值。