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

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

摘要：

• 经过40多年的努力，一个由业余爱好者组成的团队破解了著名的计算机难题——忙碌海狸难题。
• 该难题涉及寻找特定的图灵机，这种机器在停止前能写下最多的1。图灵机是计算理论中的一个抽象计算模型。
• 数学家陶哲轩认为这一成就展示了证明助手在数学研究中的重要性。
• 团队利用Coq证明助手软件，经过全球20多名贡献者的努力，找到了第五个忙碌海狸图灵机，其编号为BB(5)，能在停止前写下47,176,870个“1”。
• 这一发现被认为是自1983年以来忙碌海狸函数研究中最重要的进展。
• 忙碌海狸游戏由数学家Tibor Radó在1962年提出，旨在探索计算理论的边界。
• 早期的研究者如Allen Brady通过编写程序和使用高性能计算机来模拟图灵机的行为，为后续的研究奠定了基础。
• 2022年，研究生Tristan Stérin发起的“忙碌海狸挑战”项目，通过在线合作的方式，最终确定了BB(5)的值。
• 研究者们正在起草学术论文，以人类可读的形式补充Coq证明，并探讨BB(6)的可能性。

文章链接：点击访问