业余玩家打破图灵机40年未解难题 陶哲轩狂赞软件辅助证明

一群业余爱好者使用Coq证明助手软件成功验证了忙碌海狸问题中的第五个数BB（5）为47,176,870，这是自1983年以来计算理论领域最重要的进展。此成就标志着对复杂数学问题解决能力的提升，展示了软件辅助证明的潜力。忙碌海狸问题源于1974年，旨在寻找能够写下最多"1"的特定图灵机。问题的核心在于理解图灵机行为，特别是它们在停机问题上的表现。这一发现不仅在学术界引起轰动，也揭示了计算理论边界。研究者们正在撰写学术论文，总结这一过程，并考虑将探索第六个忙碌海狸作为下一个目标。