主要观点总结
业余爱好者们利用Coq证明助手证明了第五台忙碌海狸图灵机的存在，这台机器在4700万步后停止。他们通过在线合作，使用了加速的图灵机模拟技术，经过一系列突破，最终确定了BB(5)的值。这个故事涉及到了图灵机的概念、忙碌海狸游戏的起源、早期挑战者以及长达数十年的寻找过程。目前研究者正在起草学术论文，同时也在探索BB(6)的可能性，并发现了一个与著名数学难题科拉茨猜想相似的六规则图灵机。
关键观点总结
关键观点1: 业余爱好者们证明了第五台忙碌海狸图灵机的存在。
他们使用Coq证明助手，最终确定了BB(5)的值，即这台图灵机在停止前能够执行4700万步。
关键观点2: 在线合作和加速的图灵机模拟技术是关键。
研究者们通过在线合作，使用了一系列技术和工具，包括家谱方法、封闭磁带语言方法以及加速模拟技术等，最终取得了突破。
关键观点3: 忙碌海狸问题的历史背景。
这个问题起源于计算机科学家和图灵奖得主艾伦·图灵提出的图灵机概念，以及Tibor Radó的忙碌海狸游戏。这个游戏旨在通过模拟不同规则数量的图灵机的运行，寻找运行时间最长的机器，即“忙碌海狸”。早期的研究者如Allen Brady和Tibor Radó的学生们曾投身这个问题，经历了数十年的探索和挑战。
关键观点4: BB(5)的确认和BB(6)的探索。
经过长时间的寻找，BB(5)的值终于被确认。但目前的研究者正在探索BB(6)的可能性，并发现了一个与著名数学难题科拉茨猜想相似的六规则图灵机。
文章预览
一水 发自 凹非寺 量子位 | 公众号 QbitAI 40多年的计算机难题——忙碌海狸难题，被一群 业余爱好者 攻破 了！ 数学大佬陶哲轩转发了这一消息，并欣慰表示： 这再一次体现了证明助手对于数学研究的协作是多么有用。 计算机科学家Scott Aaronson为此还写了一篇博文，并大肆赞赏： 这个发现是自1983年以来，忙碌海狸函数研究中最重要的进展。 具体而言，人们历经数十年努力，终于找到了 第五个 “忙碌海狸”图灵机： BB(5) =47,176,870 （5状态图灵机，能在停下来之前写下47,176,870个“1”） 图灵机是一种抽象的计算模型，通过 读取和写入0和1 在无限磁带上进行计算。 早在 40多年前 ，一群计算机科学家在德国多特蒙德举行竞赛，寻找“忙碌海狸”图灵机。 找出一个特定的图灵机，在它停止之前能够写下最多的1 （我们称之为忙碌海狸数） 。 通过找出特
………………………………
