40年图灵机难题被业余玩家攻破，陶哲轩：软件辅助证明改变规则
原文中文，约4400字，阅读约需11分钟。
📝
内容提要
40年来，一群业余爱好者攻破了计算机难题——忙碌海狸难题，找到了第五个“忙碌海狸”图灵机，能在停下来之前写下47,176,870个“1”。这一成就得到了数学家和计算机科学家的赞赏。忙碌海狸游戏是为了研究图灵机的停机问题而提出的，目标是确定每个组中的“忙碌海狸数”。这一发现引发了人们对于下一个忙碌海狸数的探索。
❓
Q&A
忙碌海狸难题的核心是什么？
忙碌海狸难题旨在研究图灵机的停机问题，确定每个组中的忙碌海狸数。
第五个忙碌海狸数是什么？
第五个忙碌海狸数为BB(5) = 47,176,870。
谁参与了忙碌海狸挑战并取得了成果？
研究生Tristan Stérin发起了挑战，20多名业余爱好者参与并最终确定了BB(5)。
陶哲轩对这一成就有什么看法？
陶哲轩表示这一成就体现了证明助手在数学研究中的重要性。
忙碌海狸游戏是如何进行的？
游戏通过选择规则数量的图灵机，观察其在停止前写下的1的数量来确定忙碌海狸数。
使用了什么工具来证明BB(5)的结果？
团队使用了Coq证明助手软件来确保结果的准确性。
🏷️
