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

98 0 0

文章摘要

一群业余爱好者成功解决了困扰计算机科学家40多年的忙碌海狸难题，这一成就得到了数学家陶哲轩和计算机科学家Scott Aaronson的高度评价。忙碌海狸问题起源于1962年，由数学家Tibor Radó提出，旨在通过图灵机模型探索计算理论的边界。图灵机是一种抽象的计算模型，通过读取和写入0和1在无限磁带上进行计算。忙碌海狸问题的核心是找出在停止前能写下最多1的图灵机，这些数字被称为忙碌海狸数。

1974年确定了第四个忙碌海狸数后，寻找第五个数成为了一个未解之谜。2022年，研究生Tristan Stérin发起了“忙碌海狸挑战”，通过在线合作的方式，利用Coq证明助手软件，最终确定了第五个忙碌海狸数BB(5)为47,176,870。这一发现是自1983年以来该领域最重要的进展。

解决这一难题的过程中，贡献者们采用了多种方法和技术，包括家谱方法、封闭磁带语言方法和Coq证明助手。其中，Coq证明助手的使用显著提高了证明的严格性和可靠性。此外，研究者们还发现了与科拉茨猜想相似的六规则图灵机，这可能预示着BB(6)的探索将更加困难。

目前，相关研究者正在起草一份学术论文，以补充Coq证明的人类可读版本。尽管BB(5)已经确认，但BB(6)的探索仍在继续，这表明忙碌海狸问题的研究远未结束，它将继续推动计算理论的发展。