在计算机科学的一个神秘领域,一个长达四十年的难题——忙碌海狸问题,最近被一群业余爱好者成功破解。这一成就不仅在学术界引起了轰动,也得到了著名数学家陶哲轩的认可,他在社交媒体上转发了这一消息,并强调了证明助手在数学研究中的重要性。
计算机科学家Scott Aaronson也对这一发现给予了高度评价,认为这是自1983年以来,忙碌海狸函数研究中最重要的进展。这一成就标志着对计算理论边界的深入理解,也展示了软件辅助证明在解决复杂数学问题中的潜力。
忙碌海狸问题起源于40多年前的德国多特蒙德,当时计算机科学家们试图寻找能够在停止前写下最多"1"的特定图灵机。图灵机是一种抽象的计算模型,由艾伦·图灵在1936年提出,通过读取和写入0和1在无限长的磁带上进行计算。
1974年,第四个忙碌海狸数被确定后,寻找第五个海狸成了一个悬而未决的问题。现在,一个由20多名来自世界各地的贡献者组成的在线社区,使用名为Coq的证明助手软件,成功验证了第五个忙碌海狸数BB(5)的值为47,176,870。
这一成就不仅令社区沸腾,也引起了计算机科学家Damien Woods的惊叹,他将这一进展比作博尔特的速度。尽管这个问题的解决可能不会直接应用于计算机科学的其他领域,但对于参与者来说,这场与数学不可能性的斗争本身就是最大的奖励。
忙碌海狸问题的核心在于理解图灵机的行为,特别是它们在停机问题上的表现。图灵机的行为由一组规则定义,这些规则可以想象成一张表。每条规则指定了在特定状态下,读写头遇到0或1时应该执行的操作。
尽管图灵机可能会陷入无限循环,但确定它们是否会停止运行是一个著名的未解问题。数学家Tibor Radó不满意这个结论,并由此发明了“忙碌的海狸游戏”,通过将图灵机根据它们拥有的规则数量进行分组,来探索停机问题的本质。
早期的研究者,如Allen Brady,通过编写程序模拟图灵机的行为,对这一问题进行了探索。他的工作和其他研究者的发现,为后来的探索者奠定了基础。
直到2022年,研究生Tristan Stérin发起了“忙碌海狸挑战”,这是一个在线合作项目,旨在最终确定BB(5)。通过创新的方法和Coq证明助手的帮助,这个团队最终成功找到了第五个忙碌海狸。
这一成就不仅是对数学不可能性的挑战,也是对计算机科学极限的探索。随着BB(5)的确认,研究者们正在起草一份学术论文,这将是一个补充Coq证明的人类可读版本。同时,他们也在思考,BB(6)的探索是否将成为下一个目标。
参考资料:https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/