陶哲轩转赞！40多年「忙碌海狸」数学难题获突破，4万行Coq代码立大功

声明:本文来自于微信公众号 新智元（ID:AI_era），作者:新智元，授权「BB（5）的Coq证明已经完成」。

一分钟后，Stérin回复了一串七个感叹号。

在几周内，mxdys完善了社区的技术，并将他们的结果综合成一个40，000行的Coq证明。

法国国家研究院Inria的Coq专家Yannick Forster在审查证明后表示，「这不是一件容易形式化的事，我仍对此感到惊讶」。

Marxen和Buntrock在30多年前发现的那台在4700万步后停止运转的图灵机，确实是第五个忙碌海狸。

「这个消息对我来说非常令人兴奋，」Georgiev在一封电子邮件中写道。「我从未想到这个问题会在我有生之年得到解决。」

但对另一位忙碌海狸挑战的开创者来说，这个消息来得太晚了。

Allen Brady于4月21日去世，距离证明完成不到一个月，享年90岁。

贡献人员名单

以下是所有参与这次证明BB（5）=47176870的贡献人员名单。

下一步探索

忙碌海狸挑战的参与者们已经开始起草一篇正式的学术论文，描述他们的成果，并用更易理解的证明来补充mxdys的Coq证明。

这将需要一些时间:大多数图灵机通过多种方法被证明不会停止，团队需要决定如何最佳地将这些结果组合成一个完整的证明。

与此同时，部分团队成员已经开始研究下一个忙碌海狸。

然而就在四天前，mxdys和另一位名为Racheline的贡献者发现了BB（6）的一个似乎无法逾越的障碍:一个六规则图灵机，其停机问题类似于一个著名的数学难题——Collatz猜想。

图灵机与Collatz猜想之间的联系，可以追溯到1993年数学家Pascal Michel的一篇论文。

但新发现的图灵机，被称为「Antihydra」，是迄今为止最小的一个，似乎在没有数学上的概念性突破的情况下无法解决。

论文地址:https://link.springer.com/article/10.1007/BF01409968

显然，可以想象的到，BB（5）将是我们所知道的最后一个忙碌海狸的数字。

忙碌海狸问题有许多不同的变种，一些忙碌海狸挑战的参与者计划继续研究这些变种。但并不是所有人都打算继续这项工作。

他们各自因为不同的原因参与到这个项目中，现在他们的研究道路开始分道扬镳。

Stérin希望开发软件工具，以促进其他数学领域的在线协作。

他表示，「忙碌海狸挑战带给我的是一种非常深刻的信念，它是一种非常有效的研究方式」。

参考资料:

https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/

https://mathstodon.xyz/@TaliaRinger/112719444060361451