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

AIGC动态4周前发布 QbitAI
153 0 0
40年图灵机难题被业余玩家攻破,陶哲轩:软件辅助证明改变数学研究规则

 

文章摘要


【关 键 词】 忙碌海狸图灵机计算理论Coq证明科研进展

一群业余爱好者成功解决了困扰计算机科学家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)的探索仍在继续,这表明忙碌海狸问题的研究远未结束,它将继续推动计算理论的发展。

豆包-智能助手

原文和模型


【原文链接】 阅读原文 [ 3472字 | 14分钟 ]
【原文作者】 量子位
【摘要模型】 moonshot-v1-32k
【摘要评分】 ★★★☆☆

© 版权声明

相关文章

暂无评论

暂无评论...