40年图灵机难题被业余玩家攻破，陶哲轩：软件辅助证明改变数学研究规则

AIGC动态欢迎阅读

原标题：40年图灵机难题被业余玩家攻破，陶哲轩：软件辅助证明改变数学研究规则
关键字：图灵机,机器,规则,程序,贡献者
文章来源：量子位
内容字数：0字

内容摘要：

一水 发自 凹非寺量子位 | 公众号 QbitAI40多年的计算机难题——忙碌海狸难题，被一群业余爱好者攻破了！
数学大佬陶哲轩转发了这一消息，并欣慰表示：
这再一次体现了证明助手对于数学研究的协作是多么有用。
计算机科学家Scott Aaronson为此还写了一篇博文，并大肆赞赏：
这个发现是自1983年以来，忙碌海狸函数研究中最重要的进展。
具体而言，人们历经数十年努力，终于找到了第五个“忙碌海狸”图灵机：
BB(5) =47,176,870（5状态图灵机，能在停下来之前写下47,176,870个“1”）
图灵机是一种抽象的计算模型，通过读取和写入0和1在无限磁带上进行计算。
早在40多年前，一群计算机科学家在德国多特蒙德举行竞赛，寻找“忙碌海狸”图灵机。
找出一个特定的图灵机，在它停止之前能够写下最多的1（我们称之为忙碌海狸数）。
通过找出特定状态下能在停止前写下最多1的图灵机，我们能更好地理解计算理论的边界。
自从1974年确定了第四个忙碌海狸数后，寻找第五个成了悬而未决的问题。
而现在，来自世界各地的20多名贡献者（其中大多数人没有传统的学术资格），使用一款名为Coq证明助手

原文链接：40年图灵机难题被业余玩家攻破，陶哲轩：软件辅助证明改变数学研究规则

联系作者

文章来源：量子位
作者微信：
作者简介：