量子位
·
40年图灵机难题被业余玩家攻破，陶哲轩：软件辅助证明改变规则
内容提要
40年来，一群业余爱好者攻破了计算机难题——忙碌海狸难题，找到了第五个“忙碌海狸”图灵机，能在停下来之前写下47,176,870个“1”。这一成就得到了数学家和计算机科学家的赞赏。忙碌海狸游戏是为了研究图灵机的停机问题而提出的，目标是确定每个组中的“忙碌海狸数”。这一发现引发了人们对于下一个忙碌海狸数的探索。
关键要点
-
40多年的忙碌海狸难题被业余爱好者攻破，发现第五个忙碌海狸图灵机。
-
第五个忙碌海狸数为BB(5) = 47,176,870，能在停下来之前写下47,176,870个'1'。
-
忙碌海狸游戏旨在研究图灵机的停机问题，确定每个组中的忙碌海狸数。
-
这一成就得到了数学家和计算机科学家的赞赏，尤其是陶哲轩和Scott Aaronson。
-
图灵机是计算模型，通过读取和写入0和1进行计算，停机问题是其核心研究内容。
-
忙碌海狸游戏由数学家Tibor Radó于1962年提出，旨在简化停机问题的研究。
-
早期挑战者Allen Brady在1964年证明了BB(3) = 21，并在1974年发现了BB(4) = 107。
-
2022年，研究生Tristan Stérin发起了“忙碌海狸挑战”，最终确定了BB(5)。
-
团队使用Coq证明助手软件进行证明，确保了结果的准确性。
-
BB(5)的确认引发了对下一个忙碌海狸数BB(6)的探索，相关研究仍在继续。
延伸问答
忙碌海狸难题的核心是什么？
忙碌海狸难题旨在研究图灵机的停机问题，确定每个组中的忙碌海狸数。
第五个忙碌海狸数是什么？
第五个忙碌海狸数为BB(5) = 47,176,870。
谁参与了忙碌海狸挑战并取得了成果？
研究生Tristan Stérin发起了挑战，20多名业余爱好者参与并最终确定了BB(5)。
陶哲轩对这一成就有什么看法？
陶哲轩表示这一成就体现了证明助手在数学研究中的重要性。
忙碌海狸游戏是如何进行的？
游戏通过选择规则数量的图灵机，观察其在停止前写下的1的数量来确定忙碌海狸数。
使用了什么工具来证明BB(5)的结果？
团队使用了Coq证明助手软件来确保结果的准确性。
