说米网

40多年的计算机难题——繁忙海狸难题，被一群业余爱好者攻破了!
数学大佬陶哲轩转发了这一音讯，并欣慰表明:
这再一次表现了证明帮手关于数学研讨的协作是多么有用。
图片
计算机科学家Scott Aaronson为此还写了一篇博文，并大肆欣赏:
这个发现是自1983年以来，繁忙海狸函数研讨中最重要的进展。
图片
详细而言，人们历经数十年努力，总算找到了第五个“繁忙海狸”图灵机:
BB（5） =47，176，870(5状况图灵机，能在停下来之前写下47，176，870个“1”)
图灵机是一种笼统的计算模型，经过读取和写入0和1在无限磁带上进行计算。
图片
早在40多年前，一群计算机科学家在德国多特蒙德举办竞赛，寻觅“繁忙海狸”图灵机。
找出一个特定的图灵机，在它中止之前可以写下最多的1（咱们称之为繁忙海狸数）。
经过找出特定状况下能在中止前写下最多1的图灵机，咱们能更好地了解计算理论的边界。
自从1974年承认了第四个繁忙海狸数后，寻觅第五个成了悬而未决的问题。
而现在，来自世界各地的20多名贡献者（其间大多数人没有传统的学术资格），运用一款名为Coq证明帮手的软件获得了结果——47，176，870，该软件证明数学证明没有错误。
这一成就瞬间令社区沸腾，其间爱尔兰梅努斯大学计算机科学家Damien Woods惊叹:
就像博尔特一样，我很惊讶他们的速度如此之快!
图片
嗯，快半个世纪过去了还算快?只能说这个问题雀食有亿点难。
别着急，且看这群人怎么长江后浪推前浪抓住“第5只海狸”~
为什么提出“繁忙海狸”?

要回答这个问题，首要需求简略了解一下二进制图灵机。
1936年，计算机科学之父艾伦·图灵提出了图灵机——
由一个无限长的纸带，一个读写头（可以读取和写入纸带上的信息），以及一组内部状况等基本部分组成。
图灵机的行为由一组规矩定义，这些规矩可以幻想成一张表。表中的每行代表一个规矩，每列对应读写头读取到的符号（0或1）。
图片
每条规矩指定了在特定状况下，读写头遇到0或1时应该履行的操作。操作一般包括:
写入符号:决议在当前单元格写入什么符号（例如，将0替换为1）。
移动方向:决议读写头是向左移动、向右移动仍是坚持不动。
状况转化:决议图灵机的下一个状况是什么。
除了处理0和1的规矩外，还有一条特殊规矩告知图灵机何时中止运转。当图灵机进入这个状况时，它就不再履行任何操作，相当于“竞赛完毕”（这种状况一般不计算在状况调集里）。
而就在停机问题上，已经有研讨观察到:
一些图灵机会相对较快地中止（比方这台three-rule图灵机在11步后中止）
image.png
其他的则堕入了很简单发现的无限循环
image.png
这也启示图灵提出了闻名的“停机问题”:
图灵机是否会在有限的过程后中止运转，或许它是否会无限期地运转下去?
他还进一步说到，停机问题没有通用的处理方案，因为人们永久无法承认适用于一台机器的办法是否也适用于另一台机器。
关于这个结论，数学家Tibor Radó（以下简称拉多）不太满意，并由此发明晰“繁忙的海狸游戏”。
为了将停机问题的实质提炼成更简略的形式，拉多提出了一种办法——
将图灵机依据它们具有的规矩数量进行分组。
例如，一组代表一切只有一条规矩的图灵机，另一组代表一切有两条规矩的图灵机，依此类推。
1962年，拉多利用这些有限的图灵机组定义了“繁忙海狸游戏”。游戏的玩法是:
1.选择一个组，即承认你的图灵机将具有的规矩数量。
2.为组中的每台机器供给一个初始状况满是0的磁带。
3.观察这些机器的运转。一些机器或许会无限期地运转下去，而其他的则会在某个时刻中止。
4.在那些终究中止的机器中，有的会很快中止，有的则需求更多过程。每个组中会有一个运转时刻最长的机器，这台机器被称为“繁忙海狸”。
5.在有n条规矩的组中，这台“繁忙海狸”在中止之前所履行的步数便是所谓的“繁忙海狸数”BB（n）。
6.游戏的目标是承认这些BB（n）的切当值。
拉多给这样“极度低效”的图灵机取了一个风趣且形象的名字:繁忙海狸（Busy Beaver，取自英语中的谚语 as busy as a beaver）。
而这个游戏也终究引来一众程序员和数学爱好者的疯狂试玩。
前期吃螃蟹的人

Allen Brady（以下简称布雷迪），其时的俄勒冈州立大学数学研讨生，成了前期应战者之一。
在游戏推出前，人们已经承认了BB（1） =1，BB(2) =6，其时人们正测验攻克BB（3）。
布雷迪也投身BB（3），他编写了计算机程序来模仿图灵机的行为，这个程序构建了一种“家谱”，依据图灵机初始行为的相似性，对具有相同规矩数量的机器进行分类。
程序只在机器之间行为差异变得重要时才将家谱树分成多个分支。如果模仿显现某条分支上的机器会中止或进入无限循环，程序就会剪掉这个分支，排除那些不会无限运转下去的图灵机。
编写程序只是第一步，布雷迪需求找到足够强大的计算机来运转它。
在1964年，这不是一件简单的事。终究，他在90英里外的灵长类动物研讨实验室找到了一台SDS920计算机。
只可惜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万步后中止的图灵机。
2000年代初，一位名叫Georgi Ivanov Georgiev（化名Skelet）的保加利亚计算机科学家十分挨近这一目标。
经过两年的不懈努力，他开发了一个可以识别非中止机器新品种的计算机程序。虽然他的程序运转了一周并留下了约100个未处理的图灵机，但他手艺剖析后将名单削减到43个。
此后人们一向堕入不断测验中。
终究承认BB（5）

2022年，研讨生Tristan Stérin发起了“繁忙海狸应战”，这是一项在线协作，旨在终究承认BB（5）。
在这之前，Stérin决议在传统办法的基础上进行调整，运用布雷迪的家谱办法，并方案用独立程序处理永久运转的机器。
到2021年底，Stérin编写了第一步的计算机程序，生成了大约1.2亿台或许的图灵机列表。
为了帮助剖析这些机器，Stérin构建了一个在线界面，运用“时空图”来可视化图灵机的行为。
图片
完结这些后，鉴于个人精力有限，他在偶尔的状况下拉来了Shawn Ligocki。
Ligocki向团队介绍了关闭磁带言语办法，这是一种30年前的技能，他将其应用于当前的繁忙海狸问题。
他写了一篇博客文章介绍这项技能，但最初并不知道怎么编写一个能涵盖一切状况的程序。
然后，又一位Justin Blanchard加入了项目，他想出了怎么做到这一点，但他的程序相对缓慢。
于是别的两个贡献者找到了让它运转得更快的办法，这一技能乃至可以处理前文说到的43个未处理图灵机中的10个。
取得阶段性效果后，BB（5）总算迎来两个关键打破。
第一个是Skelet #1，它在可猜测行为和紊乱行为之间不断替换，这种特性使得它十分难以剖析和了解。
2023年3月，Ligocki和斯洛伐克贡献者Pavel Kropitz（不会说英语，运用谷歌翻译与团队其他成员交流），运用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的发现。
Coq专家Yannick Forster审查了证明，他激动表明:
我依然感到十分震惊。
图片
故事仍未完毕

BB（5）总算承认了，现在相关研讨者正在起草一份学术论文，这将是一个弥补mxdys的Coq证明的人类可读版本。
但是，BB（5）已承认，BB(6)还会远吗?
mxdys和另一位贡献者Racheline发现了一个六规矩的图灵机，其停机问题与闻名的数学难题“科拉茨猜测”相似。
为了防止让大家头疼，此处不再打开这个猜测，各位看官只需求知道它十分难就行。
以至于闻名理论计算机科学家Scott Aaronson宣布感慨:
BB（5）也许是咱们所知道的最终一个繁忙的海狸号码
嗯?这话有点耳熟，BB（4）好像也是这样说的。