陶哲轩转赞！40多年「忙碌海狸」数学难题获突破，4万行Coq代码立大功

【新智元导读】「忙碌海狸」难题困扰了计算机科学家40多年。如今，来自全球各地20 业余开发者和数学家们，终于取得了突破性进展。他们抓到了第五只忙碌海狸——用Coq辅助证明，得到答案47176870。对此陶哲轩激动地表示，这再次体现了证明助手对数学研究协作的重要性。

40多年的计算机难题——「忙碌海狸」难题，今天获得了重大突破了!

著名数学家陶哲轩转发了这一消息，欣慰地表示:这再一次体现了证明助手对于数学研究的协作是有多么有用。

计算机科学家Scott Aaronson为此还写了一篇博文，并称「这个发现是自1983年以来『忙碌海狸』函数研究中最重要的进展」。

40年前，100多名计算机科学家在西德的多特蒙德市，参加了这样一场奇怪的竞赛，选手需要捕捉一种难以捉摸的目标——忙碌海狸。

这次竞赛难度极大，因为只有四只海狸被成功捕获，第五只忙碌海狸逃脱了。

其实，这些海狸其实是一种看起来简单、运行时间奇长的计算机程序。这些程序异常活跃，对它们的搜索过程，涉及到了一些最著名的数学未解之谜。

甚至可以说，海狸难题直接根植于一个和计算机科学本身一样古老的不可解问题。

虽然我们知道自己无法战胜数学定律，但我们希望赢得一场战斗。

——三位参赛者

两年前，一位名叫Tristan Stérin的研究生建起一个网站，再次向全世界发起忙碌海狸挑战赛。

今天，有团队宣布——他们成功捕捉到了「第五只忙碌海狸」!这是由20多位来自世界各地业余爱好者组成的团队。

答案是47176870

具体来说，他们验证了一个名为BB（5）的数字的真值，这个数字量化了第五只海狸的忙碌程度。

获得这个结果的过程中，团队使用一个名为Coq的证明助手软件，后者可以确保数学证明没有错误。

圣塔菲研究所的计算机科学家Cristopher Moore这样评价:「他们为了达到目标所进行的社会学和数学工程，实在令人印象深刻」

「我惊讶于他们完成得如此之快，」爱尔兰梅努斯大学的计算机科学家、Stérin的导师Damien Woods说。「这简直达到了Usain Bolt的水平。」

可以说，寻找忙碌海狸最终是一场为了荣誉的狩猎。

因为，BB（5）的具体数值在计算机科学的其他领域并没有任何用处。

但对于捕捉忙碌海狸的猎人来说，战胜数学不可能性后取得的胜利，本身就是回报。

停机，还是不停机

牵动广大忙碌海狸猎人的程序，不是用普通编程语言编写的，而是为图灵机编写的指令。

计算机科学家艾伦·图灵在1936年设计了图灵机，从而以数学方式为计算过程建模。

图灵机的计算方式，是在无限长的磁带上读取和写入0和1。磁带被划分为多个方形单元格，一个「读写头」一次可以操作一个单元格。

每台图灵机都有一套独特的规则。

每条规则规定了读写头在进入一个新的单元格时应该做什么，取决于它遇到的是0还是1。

这意味着，图灵机的指令可以用一个表格来总结，每条规则占一行，两列分别对应读写头遇到0和遇到1的情况。

一条规则可能是:「如果读到0，将其替换为1，向右移动一步，并参照规则C」，这是第一列。

「如果读到1，保持不变，向左移动一步，并参照规则A」，这是第二列。

所有规则都如此，除非某个特殊规则告诉机器何时停止运行。

不过，虽然图灵机有停机的方法，但并不意味着它会停。

在最简单的情况下，它可能会陷入一个无限循环中，不断循环几个状态。

是否存在这样一种方法，可以判断具有特定规则集的图灵机是会停机，还是会永远运行下去呢?

这，就是著名的停机问题的本质，也是使得海狸难题如此迷人的原因。

图灵证明了停机问题没有普遍的解决方案——我们永远无法确定，对一台机器有效的方法是否对另一台机器也同样有效。

好在，停机问题并不总是对特定的机器来说很难。

比如下面这个视频中，有些机器会相对较快地停机。

而有的机器却很快陷入了无限循环。

这台三规则图灵机很快陷入了无限循环

我们总会遇到一些难以轻易分类的图灵机——它的运行会很快结束，还是会在磁带上永远徘徊?

是的，除非它运行足够长的时间，否则我们根本不知道，它会做什么。

忙碌海狸，在不可知边缘探索

忙碌海狸的故事，始于数学家Tibor Radó。

1895年出生于匈牙利，大学学习的是土木工程。一战爆发后，在西伯利亚战俘营的同伴指导下开始学习数学

后来他重返校园，在俄亥俄州立大学任教35年。

关于停机问题，他对图灵的证明并不满意。

为了将这个问题的本质提炼得更简单，Radó希望根据图灵机的规则数量进行分类——所有一规则图灵机为一组，所有二规则图灵机为另一组，依此类推。

如此一来，虽然会因图灵机可以有任意数量的规则而被分成无限多的组，但由于规则的组合是有限的，所以每组中的不同机器数量也是有限的。

这样推理，就比考虑所有的机器容易多了。

在1962年的一篇论文中，Radó基于此提出了「忙碌海狸游戏」。

要进行这个游戏，首先需要选择一个组——也就是你机器的规则数量。

给组中的每台机器提供一条每个单元格都是0的磁带后，有些机器会一直运行下去，其余的最终会停机。

其中有些会很快停机，有些会花更长时间，而有一台会是最后一个停机的。每个组都会有一个运行时间最长的成员，这些特别勤奋的机器，就被称为「忙碌海狸」。

在拥有n条规则的组中，忙碌海狸机器在停机前所需的步数，就是相应的忙碌海狸数BB（n）。而游戏的目标，是确定这些数字的确切值。

仔细一想就知道，解决「忙碌海狸」需要考虑众多问题。

要成功的话，你必须确定每台停机机器的运行时间，看看哪台花费的时间最长。你还必须证明所有其他的机器永远不会停机。

测量运行时间当然很简单，因为在普通计算机上模拟图灵机很容易。

但是，想要证明一台机器永远运行下去，相当于为它解决停机问题的具体版本——在最一般形式下，这几乎是不可能完成的任务。

「我们在不可知的边缘进行探索，」软件工程师、海狸难题的贡献者Shawn Ligocki这样说。

但不可知性究竟从哪里开始?

只有几个规则的图灵机看起来非常简单。理解一个可以放在索引卡上的程序有多难?

数学研究生的海狸团队

单一规则的情况很简单，因为实际上只有两种可能性。

如果规则告诉图灵机在看到0时停机，它会在第一步就停止。任何其他规则都会导致机器永远在磁带上前进，因为它会在每个单元格中遇到0。这意味着BB（1） =1。

除了这个小海狸，一个只用铅笔和纸装备的猎人很快就会遇到问题。对于两规则的情况，已经有超过6000个不同的图灵机需要考虑;这个数字在三规则时膨胀到数百万，在四规则时膨胀到数十亿。

手工处理所有这些情况是不可能的。「显然，你不可能做到这一点，」Ligocki说。「即使你能做到，也没有人会相信你。」

这意味着，这个根植于计算基础的问题只能在计算机的帮助下解决。

是的，一个相当简单的程序足以证明BB（2） =6，但从BB(3)起，就开始变得困难多了。

而Radó介绍这个游戏后不久，一小部分研究人员开始了这场狩猎。

Oregon State University的数学研究生Allen Brady很快就意识到，取得进展的关键，就是忽略图灵机之间不重要的差异。

例如，考虑一个有许多规则的图灵机，其中第一个规则告诉它如果读取到0就停机。

「其余那些转换中的内容并不重要，因为它会立即停机，」Ligocki说。就忙碌海狸游戏而言，这些机器大多数是多余的，因此可以直接一次性排除它们。

研究生Brady将这个过程，整合到一个用于模拟图灵机的计算机程序中。

基于机器初始行为的相似性，这个程序为具有相同规则数量的机器构建了一个类似家族树的结构。

只有当机器之间的差异变得相关时，程序才会将树分成多个分支，并删除在模拟中停机或进入无限循环的整个分支。

程序是编出来了，但找到能运行它的计算机，在1964年时并不容易。

终于，Brady获得了90英里外一个灵长类研究实验室计算机的使用权。

没想到，工作进行到一半，Brady发现自己被半路截胡了:Radó的研究生Shen Lin已经证明了第三个忙碌海狸数BB（3） =21。

Brady并未气馁，不仅确认了Lin的结果，而且在BB（4）上取得了部分突破——此前，Radó认为BB(4)「完全无望」解决。

BB（4）之所以难解，不仅是因为问题数量庞大，更因为四条规则的机器能够表现出的行为，实在是太丰富了!

所有不停机的两规则机器，都会陷入容易检测的无限循环。

在三规则的情况下，有几十台机器会永远运行而不进入循环，而证明这些机器永不停机，需要不同的方法。

对于四规则的机器，则有成千上万台这种非循环机器。

毕业后，Brady识别出了一些新的非停机图灵机种类，并给它们起了「影树」和「尾食龙」之类的奇幻名字。

1966年，他发现了一台四规则机器，在停机前运行了107步，他猜测:这就是难以捉摸的第四个忙碌海狸。

他的猜想是对的，但直到1974年，他才证明没有其他停机机器能运行得更久。

他在一份内部技术报告中写下了证明，但直到九年后，报告才在学术期刊上发表。

这是人类在超过40年里，所知道的最后一个忙碌海狸数。

第五只忙碌海狸诞生!

Brady发表证明的那一年，也是多特蒙德比赛——第一次寻找第5个忙碌海狸的大型竞赛的那一年。

对于五规则机器，可能的图灵机数量接近17万亿。即使以每毫秒一个的速度列出所有这些机器，也需要超过500年。

用Brady家谱方法来缩小搜索空间仍然必不可少，但程序必须运行得非常快，才有希望成功。

参赛者们各自开发了自己的程序，并且找到了运行时间最长的五规则图灵机——最忙的那台，在超过100，000步后停机。

《科学美国人》1984年对比赛报道后，不久后就有一位研究者打破了多特蒙德的纪录:一台机器在超过200万步后才停机。

柏林的研究生Heiner Marxen和Jürgen Buntrock，也开始利用业余时间研究这个问题。

几年后，在1989年Marxen成为了程序员，在公司中获得了一台强大的计算机。

竟然凭自己的程序找到了一台惊人的机器，在47176870步后才停机。

起初，他认为代码中肯定有错误。

但调试了几个小时后，他开始有一种奇怪的感觉:自己捕获到了忙碌海狸。

Buntrock很快复现了这一结果，两人发表了论文。

虽然Marxen捕获了忙碌海狸，但证明所有剩余的机器都不会停机，则花了超过30年。

在2000年初，一位名叫Georgi Ivanov Georgiev的保加利亚计算机科学家几乎成功了。

当时，他在一家国有电信公司担任系统管理员。他痴迷于BB（5）的研究，花了两年时间，每天花数小时改进一个可以识别新型非停机机器的程序。

最终的程序有6000行密集且没有注释的代码，运行时间超过一周。它留下了大约100台未决的图灵机。

手工分析这些机器后，他将名单缩减到43台。

2003年，Georgiev在网上发布了成果。

Marxen鼓励Georgiev继续努力，但两年的高强度工作已经让他筋疲力尽。

「这段时间结束时，我无法再产生任何新想法，我非常疲惫。」

这也是忙碌海狸研究者所共同面临的困境。

几十年来，他们或独自或成对地辛勤工作，却没有得到广泛学术界的太多认可。但是要完成这项工作，显然需要集体的努力。

召集所有猎手

召集所有猎手的努力，始于Tristan Stérin。

2000年代末，他最初通过IM结识了一位编程竞赛爱好者，从而早早精通了计算机编程。

但他很快意识到编程竞赛的文化，并不适合自己。

2022年，Tristan Stérin发起了忙碌海狸挑战赛，这是一项在线合作，旨在最终确定第五个忙碌海狸数量的价值

他表示，「我不是一个喜欢竞争的人。我喜欢看到一个问题，然后花3个月时间思考它，而不是只花30分钟」。

在好奇心的驱使下，Stérin决定从法国来到爱尔兰攻读研究生，在那里他与Woods一起研究DNA计算，即如何使用DNA链实现算法。

2020年夏天，Woods给他发了一篇关于「忙碌海狸」的综述论文，作者是计算机科学家Scott Aaronson。

Stérin立即被这篇文章吸引了。

论文地址:https://dl.acm.org/doi/10.1145/3427361.3427369

在与Woods合作撰写了一篇关于大型图灵机能力的论文后，他转向研究BB（5）问题，并下定决心要最终证明——Marxen和Buntrock的4700万步机器，确实是第五个「忙碌海狸」。

Stérin说，「我有强烈的直觉，自己做不到。但我也有一种直觉，这件事是可以做到的」。

论文地址:https://arxiv.org/pdf/2107.12475

从一开始，Stérin就知道，要有结论性的证明，必须有良好的文档记录和可重复性，因为任何微小的软件错误都会对整个研究造成致命打击。

Georgiev的程序极其复杂，但其他研究人员发现它难以解析。

参与「忙碌海狸」挑战赛的软件开发人员Justin Blanchard表示，「当你回头试图审查代码时，你会马上放弃。任何新的方法实际上都得从头开始」。他曾是一名数学专业的研究生。

Stérin决定在传统方法的基础上进行一些改进。

他首先使用Brady的家族树（Brady’s family-tree）方法，来消除冗余的图灵机，并识别出哪些机器在4700万步内停机。

但与Brady或其后继者不同的是，Stérin没有包含任何用于剔除永远运行的机器的代码。

相反，他计划使用独立的程序来解决这些问题，每种方法对应一个程序，证明图灵机永远不会停机。

这样分块处理任务，将使合作伙伴更容易独立地完成每个部分，并交叉检查结果。

2021年底，Stérin编写了第一步的计算机程序。

它生成了大约1.2亿台图灵机的列表，这些图灵机足以确定BB（5）的值——其余的都是冗余的。

在这1.2亿台图灵机中，大约1/4在Marxen和Buntrock的机器之前就停机了，剩下的8800万台仍在考虑范围内。

为了帮助分析这些图灵机，Stérin构建了一个在线界面，用于在「时空图」上可视化它们的行为，时空图是由代表0和1的黑白方格组成的二维网格。

图中的每一行记录了图灵机演化过程中的一步。

第一行代表第一步后的纸带状态，第二行显示第二步后的纸带状态，依此类推。

以这种方式查看，Stérin收集的图灵机仿佛活了过来，展示出令人眼花缭乱的各种不同模式。

要证明Marxen和Buntrock确实找到了第五个忙碌海狸，就意味着要证明这些机器中的每一个都会永远运行下去。

Stérin知道，自己无法单独完成这项任务。

2022年春天，Stérin和一些早期加入者在独立平台Discord上，创建了一个论坛和一个单独的聊天服务器。

然后，是时候寻找贡献者了。

「忙碌海狸」的魅力

Shawn Ligocki很快加入了团队。

也许这是命运:他1985年出生在Beaverton，虽然他第一次听说「忙碌海狸」是在2004年，当时在他大学第一学期结束时。

寒假期间，他和他的父亲Terry一起开始研究海狸搜索算法，Terry是劳伦斯伯克利国家实验室的一名应用数学家。

一个月后，当Ligocki回到大学忙于课程时，他的父亲兴奋地打电话给他。

他决定在Brady发明的原始忙碌海狸游戏的一个变体上，测试他们的一个算法，并发现了一台打破Brady记录的图灵机。

他们联系了已经退休的Brady，Brady很高兴并在他的网站上公布了这个结果。

随之，Shawn Ligocki很快与世界各地的「忙碌海狸」研究人员通过电子邮件进行交流。

有一次难忘的经历发生在Ligocki大二暑假访问德国期间，他顺道去了柏林与Marxen见面。

忙碌海狸的魅力，伴随着Ligocki整个大学期间，但毕业找到工作后，生活琐事让他分心。

他偶尔会重新投入忙碌海狸的研究，但从未持续太久。

2022年初，他建立了一个在线讨论组，帮助研究人员保持联系。5月时，Stérin发现了这个邮件列表，并发出加入忙碌海狸挑战的邀请。Ligocki毫不犹豫地接受了邀请。

他对项目的首次贡献之一，是复兴了Marxen发明的一种技术，这是他们16年前在柏林酒吧讨论过的技术。

这种技术被称为「封闭磁带语言」（the closed tape language）方法。这是一种新方法，用于识别图灵机磁带上永不停止的模式。

这是识别循环程序和许多其他图灵机不停机的基本策略，但「封闭磁带语言」方法有潜力通过统一的数学框架识别更广泛的模式类别。

Ligocki写了一篇博客文章，向他的新合作者介绍了这项技术，但尽管理论上的想法非常通用，他并不知道如何编写一个涵盖所有情况的程序。

Justin Blanchard在秋天加入项目后不久，就找到了方法，但他的程序相对较慢。然后另外两位贡献者找到了让它运行更快的方法。

在几个月内，「封闭磁带语言」技术从一个有前途的想法变成了他们最强大的工具之一。

它甚至可以处理Georgiev的43个未解决问题中的10个，为纪念他而被称为「Skelet图灵机」。

怪物「图灵机」来袭

随着时间的推移，新的贡献者们发现了「忙碌海狸」挑战，并开始逐步解决问题的不同部分。

但许多图灵机仍未解决，其中有两台图灵机尤其声名狼藉。

第一台是Skelet #1，它在可预测和混乱的行为之间不断交替。

在2023年3月，Ligocki和Pavel Kropitz——一位不会说英语的斯洛伐克贡献者，通过谷歌翻译与团队其他成员交流——提出了一系列想法，终于破解了它。

使用Marxen和Buntrock30年前的加速模拟技术的升级版，他们发现秩序与混乱之间的拉锯战确实结束了，但只有在超过一万亿亿步之后。

然后它最终进入了一个异常长的重复循环周期。

实际上，几乎所有的无限循环在1000步内就会开始重复;而Skelet #1的循环超过了80亿步之长。

这台图灵机的行为非常诡异，证明过程融合了许多不同的想法，以至于Ligocki在近5个月内都无法确定结果。

不过，这一不确定重复周期，被一位新贡献者打破了——一位21岁的自学成才的程序员，名叫Maja Kądziołka，多数情况在她只用一个字mei。

mei在波兰长大，并在2021年秋季在华沙大学学习了一个学期后辍学。

随后，她在一家软件公司工作了一年多，但越来越觉得工作令人筋疲力尽，开始寻找更具智力挑战的工作。

偶然的机会，她在软件Coq中找到了这种兴趣，这是一款设计用于编码和验证数学证明有效性的软件。

当时，忙碌海狸挑战的贡献者们已经在证明中使用计算机程序，但就像纸笔证明一样，计算机程序也容易出错。

而在Coq证明中，代码只有在每一行逻辑上都能从前一行推导出来时才能运行，这使得错误几乎不可能发生。

对mei来说，弄清楚如何制作这些证明开始变得像一场游戏。

在学习了Coq之后，mei开始寻找一个开放的问题来测试它。就在那时，她发现了忙碌海狸挑战。

几周后，她将团队的几项证明用Coq重新编写，包括Ligocki和Kropitz关于Skelet #1永不停止的证明——Ligocki终于可以确定这一点了。

突然间，比Stérin强调的可重复性更高的严格标准，似乎成为可能。

项目地址:https://github.com/meithecatte/busycoq

而这一切都是由一个没有正式训练的人——一个业余数学家做出来的。

突破性进展

大约在同一时间，一位名叫Chris Xu的研究生，在第二台怪物图灵机——Skelet #17上取得了突破。

通常，即使是复杂的五规则图灵机（five-rule Turing machines），一旦理解了其工作原理，总结其行为也不难。

通过研究Skelet #17磁带上的模式来理解它，就像解密四层加密的秘密信息一样:破解一个代码只是揭示了另一个完全不相关的代码，并且下面还有两个。

Xu必须解密所有这些代码，才能最终证明这台机器从未停止。

Xu的证明非常出色，但它涉及一些无人知道，如何用Coq所要求的精确术语形式化的数学直觉。

而且，忙碌海狸挑战的工作还远未完成:虽然Skelet #1和#17是看起来最难对付的两台图灵机，但还有其他一些图灵机需要解决，还有一些只使用低效程序解决的图灵机。

这不足以说服世界。

在接下来的几个月里，社区慢慢拼凑出剩余图灵机的证明，但大多数还没有被翻译成Coq。

然后在四月，一个神秘的新贡献者出现了，他用化名mxdys来完成这项工作。

团队中没有人知道mxdys的所在地或其他个人信息。在一次Discord私信交流中，他提到对数学游戏有长期兴趣，但拒绝提供更多关于他背景的信息。

5月10日，mxdys在Discord服务器上发布了一条简短的消息:「BB（5）的Coq证明已经完成」。

一分钟后，Stérin回复了一串七个感叹号。

在几周内，mxdys完善了社区的技术，并将他们的结果综合成一个40，000行的Coq证明。

法国国家研究院Inria的Coq专家Yannick Forster在审查证明后表示，「这不是一件容易形式化的事，我仍对此感到惊讶」。

Marxen和Buntrock在30多年前发现的那台在4700万步后停止运转的图灵机，确实是第五个忙碌海狸。

「这个消息对我来说非常令人兴奋，」Georgiev在一封电子邮件中写道。「我从未想到这个问题会在我有生之年得到解决。」

但对另一位忙碌海狸挑战的开创者来说，这个消息来得太晚了。

Allen Brady于4月21日去世，距离证明完成不到一个月，享年90岁。

贡献人员名单

以下是所有参与这次证明BB（5）=47176870的贡献人员名单。

下一步探索

忙碌海狸挑战的参与者们已经开始起草一篇正式的学术论文，描述他们的成果，并用更易理解的证明来补充mxdys的Coq证明。

这将需要一些时间:大多数图灵机通过多种方法被证明不会停止，团队需要决定如何最佳地将这些结果组合成一个完整的证明。

与此同时，部分团队成员已经开始研究下一个忙碌海狸。

然而就在四天前，mxdys和另一位名为Racheline的贡献者发现了BB（6）的一个似乎无法逾越的障碍:一个六规则图灵机，其停机问题类似于一个著名的数学难题——Collatz猜想。

图灵机与Collatz猜想之间的联系，可以追溯到1993年数学家Pascal Michel的一篇论文。

但新发现的图灵机，被称为「Antihydra」，是迄今为止最小的一个，似乎在没有数学上的概念性突破的情况下无法解决。

论文地址:https://link.springer.com/article/10.1007/BF01409968

显然，可以想象的到，BB（5）将是我们所知道的最后一个忙碌海狸的数字。

忙碌海狸问题有许多不同的变种，一些忙碌海狸挑战的参与者计划继续研究这些变种。但并不是所有人都打算继续这项工作。

他们各自因为不同的原因参与到这个项目中，现在他们的研究道路开始分道扬镳。

Stérin希望开发软件工具，以促进其他数学领域的在线协作。

他表示，「忙碌海狸挑战带给我的是一种非常深刻的信念，它是一种非常有效的研究方式」。

参考资料:

https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/

https://mathstodon.xyz/@TaliaRinger/112719444060361451