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

主要观点总结

文章介绍了计算机科学家和业余爱好者们成功确定了五繁忙海狸（BB(5)）图灵机的运行时间，通过一种被称为Coq证明助手的软件来验证了一个特定的六状态图灵机的行为，从而解决了困扰学界多年的难题。文章还提到了该成就的历程、前期面临的挑战和未解决的问题。

关键观点总结

关键观点1: 业余爱好者破解了计算机难题

一群业余爱好者使用Coq证明助手软件成功破解了寻找第五个忙碌海狸图灵机的难题，确认了BB(5)的值。

关键观点2: 关于忙碌海狸的研究历程

文章回顾了自寻找第五个忙碌海狸开始的历程，包括早期计算机科学家如Allen Brady和Tibor Radó的工作，以及近年来不同研究者对BB(5)的突破。

关键观点3: 解决难题的方法和工具

文章描述了用于确定BB(5)的新技术和工具，如Marxen和Buntrock的图灵机模拟加速技术，以及神秘新贡献者mxdys的Coq证明。

关键观点4: 未来的挑战和可能性

文章探讨了未来的挑战，包括确定BB(6)的值以及解决类似著名数学难题“科拉茨猜想”等相关问题。