第五个 Busy Beaver 值的确定
计算机科学中的逻辑
2026-03-24 v2 形式语言与自动机理论
逻辑
摘要
Busy Beaver 值 是 态 2 符号图灵机从全零纸带开始运行并在停机前可执行的最大步数。 历史上由 Tibor Rad\'o 于 1962 年引入，作为不可计算函数的最简单示例之一。我们使用 Coq 证明助手证明了 。该证明枚举了 个 5 态图灵机，并对每台机器判定其是否停机。我们的结果标志着 40 多年来首次确定新的 Busy Beaver 值，也是有史以来首次被形式化验证的 Busy Beaver 值，证明了大规模协作在线研究 (bbchallengeorg) 的有效性。
关键词
引用
@article{arxiv.2509.12337,
title = {Determination of the fifth Busy Beaver value},
author = {The bbchallenge Collaboration and Justin Blanchard and Daniel Briggs and Konrad Deka and Nathan Fenner and Yannick Forster and Georgi Georgiev and Matthew L. House and Rachel Hunter and Iijil and Maja Kądziołka and Pavel Kropitz and Shawn Ligocki and mxdys and Mateusz Naściszewski and savask and Tristan Stérin and Chris Xu and Jason Yuen and Théo Zimmermann},
journal= {arXiv preprint arXiv:2509.12337},
year = {2026}
}
备注
48 pages, 17 figures