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

AIGC动态欢迎阅读

原标题：陶哲轩转赞！40多年「忙碌海狸」数学难题获突破，4万行Coq代码立大功
关键字：图灵机,机器,报告,规则,程序
文章来源：新智元
内容字数：0字

内容摘要：

新智元报道编辑：编辑部
【新智元导读】「忙碌海狸」难题困扰了计算机科学家40多年。如今，来自全球各地20+业余开发者和数学家们，终于取得了突破性进展。他们抓到了第五只忙碌海狸——用Coq辅助证明，得到答案47176870。对此陶哲轩激动地表示，这再次体现了证明助手对数学研究协作的重要性。40多年的计算机难题——「忙碌海狸」难题，今天获得了重大突破了！
著名数学家陶哲轩转发了这一消息，欣慰地表示：这再一次体现了证明助手对于数学研究的协作是有多么有用。
计算机科学家Scott Aaronson为此还写了一篇博文，并称「这个发现是自1983年以来『忙碌海狸』函数研究中最重要的进展」。
40年前，100多名计算机科学家在西德的多特蒙德市，参加了这样一场奇怪的竞赛，选手需要捕捉一种难以捉摸的目标——忙碌海狸。
这次竞赛难度极大，因为只有四只海狸被成功捕获，第五只忙碌海狸逃脱了。
其实，这些海狸其实是一种看起来简单、运行时间奇长的计算机程序。这些程序异常活跃，对它们的搜索过程，涉及到了一些最著名的数学未解之谜。
甚至可以说，海狸难题直接根植于一个和计算机科学本身一样古老的不可解问题。
虽然我们知

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