40年图灵机难题被业余玩家攻破，陶哲轩：软件辅助证明改变规则
原文中文，约4400字，阅读约需11分钟。
📝
内容提要
40年来，一群业余爱好者攻破了计算机难题——忙碌海狸难题，找到了第五个“忙碌海狸”图灵机，能在停下来之前写下47,176,870个“1”。这一成就得到了数学家和计算机科学家的赞赏。忙碌海狸游戏是为了研究图灵机的停机问题而提出的，目标是确定每个组中的“忙碌海狸数”。这一发现引发了人们对于下一个忙碌海狸数的探索。
🔎
延伸解读
业余爱好者如何攻克难题
文章指出，来自世界各地的20多名贡献者中，大多数人没有传统的学术资格。他们通过在线合作，使用Coq证明助手软件，最终确定了BB(5)的值。这表明，在软件辅助下，非专业研究者也能对复杂数学问题做出重要贡献。
证明助手的关键作用
陶哲轩转发消息时表示，这体现了证明助手对数学研究的协作非常有用。团队使用Coq验证了证明没有错误，其中一位贡献者mxdys在几周内完成了40,000行的Coq证明。这提高了结果的可靠性，并改变了数学证明的协作方式。
BB(5)的确认与后续挑战
BB(5) = 47,176,870的确认结束了自1974年确定BB(4)以来长达数十年的悬而未决。目前研究者正在起草学术论文，以提供人类可读的证明版本。同时，对BB(6)的探索已经开始，有贡献者发现了一个与科拉茨猜想相似的六规则图灵机，其难度可能更大。
❓
Q&A
忙碌海狸难题的核心是什么？
忙碌海狸难题旨在研究图灵机的停机问题，确定每个组中的忙碌海狸数。
第五个忙碌海狸数是什么？
第五个忙碌海狸数为BB(5) = 47,176,870。
谁参与了忙碌海狸挑战并取得了成果？
研究生Tristan Stérin发起了挑战，20多名业余爱好者参与并最终确定了BB(5)。
陶哲轩对这一成就有什么看法？
陶哲轩表示这一成就体现了证明助手在数学研究中的重要性。
忙碌海狸游戏是如何进行的？
游戏通过选择规则数量的图灵机，观察其在停止前写下的1的数量来确定忙碌海狸数。
使用了什么工具来证明BB(5)的结果？
团队使用了Coq证明助手软件来确保结果的准确性。
🏷️
