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

主要观点总结

文章介绍了计算机科学家和业余爱好者们成功确定了五繁忙海狸（BB(5)）图灵机的运行时间，通过一种被称为Coq证明助手的软件来验证了一个特定的六状态图灵机的行为，从而解决了困扰学界多年的难题。文章还提到了该成就的历程、前期面临的挑战和未解决的问题。

关键观点总结

关键观点1: 业余爱好者破解了计算机难题

一群业余爱好者使用Coq证明助手软件成功破解了寻找第五个忙碌海狸图灵机的难题，确认了BB(5)的值。

关键观点2: 关于忙碌海狸的研究历程

文章回顾了自寻找第五个忙碌海狸开始的历程，包括早期计算机科学家如Allen Brady和Tibor Radó的工作，以及近年来不同研究者对BB(5)的突破。

关键观点3: 解决难题的方法和工具

文章描述了用于确定BB(5)的新技术和工具，如Marxen和Buntrock的图灵机模拟加速技术，以及神秘新贡献者mxdys的Coq证明。

关键观点4: 未来的挑战和可能性

文章探讨了未来的挑战，包括确定BB(6)的值以及解决类似著名数学难题“科拉茨猜想”等相关问题。

文章预览

点击上方“ 图灵人工智能 ”，选择“星标”公众号 您想知道的人工智能干货，第一时间送达                           一水 发自 凹非寺 转自量子位 | 公众号 QbitAI 40多年的计算机难题——忙碌海狸难题，被一群 业余爱好者 攻破 了！ 数学大佬陶哲轩转发了这一消息，并欣慰表示： 这再一次体现了证明助手对于数学研究的协作是多么有用。 计算机科学家Scott Aaronson为此还写了一篇博文，并大肆赞赏： 这个发现是自1983年以来，忙碌海狸函数研究中最重要的进展。 具体而言，人们历经数十年努力，终于找到了 第五个 “忙碌海狸”图灵机： BB(5) =47,176,870 （5状态图灵机，能在停下来之前写下47,176,870个“1”） 图灵机是一种抽象的计算模型，通过 读取和写入0和1 在无限磁带上进行计算。 早在 40多年前 ，一群计算机科学家在德国多特蒙德举行竞赛 ………………………………