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

声明:本文来自于微信公众号 新智元（ID:AI_era），作者:新智元，授权转载发布。

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

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

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

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

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

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

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

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

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

——三位参赛者

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

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

答案是47176870

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

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

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

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

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

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

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

停机，还是不停机

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

计算机科学家艾伦·图灵在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(二) =6，但从BB(3)起，就开始变得困难多了。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

毕业后，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(五)的研究，花了两年时间，每天花数小时改进一个可以识别新型非停机机器的程序。

最终的程序有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(五)问题，并下定决心要最终证明——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(五)的值——其余的都是冗余的。

在这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(五)的Coq证明已经完成。

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

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

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

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

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

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

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

贡献人员名单

以下是所有参与这次证明BB(五)=47176870的贡献人员名单。

下一步探索

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

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

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

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

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

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

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

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

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

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

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

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

参考资料:

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

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