导语：40多年前，计算机科学家在德国多特蒙德举行竞赛，寻找“忙碌海狸”图灵机。如今，这一难题被一群业余爱好者攻破，数学大佬陶哲轩转发消息表示欣慰，认为这体现了证明助手对于数学研究的协作是多么有用。
正文：
一、难题攻破
经过数十年努力，来自世界各地的20多名业余爱好者使用一款名为Coq证明助手的软件，找到了第五个“忙碌海狸”图灵机：BB(5) =47,176,870。这一成就瞬间令社区沸腾，其中爱尔兰梅努斯大学计算机科学家Damien Woods惊叹：“就像博尔特一样，我很惊讶他们的速度如此之快！”
二、忙碌海狸难题
忙碌海狸难题源于1974年，当时确定了第四个忙碌海狸数。自此，寻找第五个忙碌海狸数成为悬而未决的问题。忙碌海狸数是图灵机在停止之前所能写下的最多1的个数。
三、证明助手助力
此次攻破难题的关键在于使用Coq证明助手软件。该软件证实了数学证明没有错误，使得这一成就得以实现。
四、数学研究规则改变
这一成就对数学研究具有重要意义。它表明，业余爱好者也可以在数学领域取得突破，同时也展示了证明助手在数学研究中的重要作用。
五、忙碌海狸游戏
忙碌海狸游戏由数学家Tibor Radó在1962年发明，旨在将停机问题的本质提炼成更简单的形式。游戏的目标是确定忙碌海狸数BB(n)的确切值。
六、早期挑战者
早期挑战者之一是俄勒冈州立大学数学研究生Allen Brady。他编写了计算机程序来模拟图灵机的行为，并使用一台强大的计算机进行模拟。
结语：
40年图灵机难题被业余玩家攻破，不仅体现了数学研究的无限魅力，也展示了业余爱好者在数学领域的潜力。这一成就将为数学研究带来新的启示，也为数学界注入新的活力。
Views: 0