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

主要观点总结

业余爱好者们利用Coq证明助手证明了第五台忙碌海狸图灵机的存在，这台机器在4700万步后停止。他们通过在线合作，使用了加速的图灵机模拟技术，经过一系列突破，最终确定了BB(5)的值。这个故事涉及到了图灵机的概念、忙碌海狸游戏的起源、早期挑战者以及长达数十年的寻找过程。目前研究者正在起草学术论文，同时也在探索BB(6)的可能性，并发现了一个与著名数学难题科拉茨猜想相似的六规则图灵机。

关键观点总结

关键观点1: 业余爱好者们证明了第五台忙碌海狸图灵机的存在。

他们使用Coq证明助手，最终确定了BB(5)的值，即这台图灵机在停止前能够执行4700万步。

关键观点2: 在线合作和加速的图灵机模拟技术是关键。

研究者们通过在线合作，使用了一系列技术和工具，包括家谱方法、封闭磁带语言方法以及加速模拟技术等，最终取得了突破。

关键观点3: 忙碌海狸问题的历史背景。

这个问题起源于计算机科学家和图灵奖得主艾伦·图灵提出的图灵机概念，以及Tibor Radó的忙碌海狸游戏。这个游戏旨在通过模拟不同规则数量的图灵机的运行，寻找运行时间最长的机器，即“忙碌海狸”。早期的研究者如Allen Brady和Tibor Radó的学生们曾投身这个问题，经历了数十年的探索和挑战。

关键观点4: BB(5)的确认和BB(6)的探索。

经过长时间的寻找，BB(5)的值终于被确认。但目前的研究者正在探索BB(6)的可能性，并发现了一个与著名数学难题科拉茨猜想相似的六规则图灵机。

免责声明