※ [本文转录自 Math 看板 #1cslfIC6 ]
作者: jackliao1990 (j) 看板: Math
标题: Fw: [爆卦] 睽违50年 科学家找到第五个忙碌海狸数
时间: Fri Sep 6 20:49:21 2024
※ [本文转录自 Gossiping 看板 #1cslc5hw ]
作者: jackliao1990 (j) 看板: Gossiping
标题: [爆卦] 睽违50年 科学家找到第五个忙碌海狸数
时间: Fri Sep 6 20:45:52 2024
https://discuss.bbchallenge.org/t/july-2nd-2024-we-have-proved-bb-5-47-176-870/237
1936年资工之父图灵提出图灵机后，图灵停机问题也成为电脑科学的重要问题:"图灵机是
否会在有限步骤后停止运行，或是会无限运行下去？ "
1962年数学家Tibor Rad为了解决停机问题而发明了忙碌海狸游戏，该游戏是停机问题的简
单等价形式，破解此游戏就等于解开停机问题 。
游戏的玩法 ：
1. 选择一个群组，确定你的图灵机将拥有的规则数量。
2. 为组中每台机器提供一个初始状态全是0的磁带。
3. 观察机器。有些机器可能会无限期地运行下去，其他则会在某个时刻停止。
4. 在最终停止的机器中，每个组别中会有一个运行时间最长的机器， 这台机器被称为“
忙碌海狸” 。
5. 在有n条规则的组别中，这台“忙碌海狸”在停止之前所执行的步数就是“忙碌海狸数
”BB(n)。
6. 游戏目标是确定这些BB(n)的确切值。
科学家很快就发现BB(1) = 1，BB(2) = 6，1964年Shen Lin 证明BB(3) = 21，1974年
Allen Brady证明BB(4)=107。之后的50年各家好手持续寻找BB(5)，工程师编写识别非停
止机器新种类的程式，计算机的停止步数纪录也随着电脑实验而不断刷新-最高纪录为
1989年工作中的Heiner Marxen用一台强大计算机重新启动搜索程式时，意外发现在4700
万步停止的图灵机。
2022年Tristan Stérin也发起了 “忙碌海狸挑战”，旨在透过线上挑战来确定BB(5)。
他使用Allen Brady的家谱方法并用独立程式处理永远运行的机器。他写的第一步电脑程
式产生了1.2亿台可能图灵机清单。为了分析这些机器，Stérin建立了使用时空图来视觉
化图灵机行为的线上接口。之后加入的Shawn Ligocki和Justin Blanchard 引入封闭磁带
语言方法来处理未解决的图灵机。
最后剩下两种行为古怪、难以分析的图灵机，Ligocki等人为此卡了5个月都无法确定证明
是否正确，新加入的mei和mxdys(化名)引入了名为Coq证明助手的软件，他们将证明翻译
成Coq语言并在数周内完成了40000行的Coq证明，最终证实1989年Marxen的发现，BB(5)
=47176870。
数学界为此陷入沸腾。而对于寻找BB(6)，mxdys和Racheline发现了一个六规则的图灵机
，其停机问题类似考拉兹猜想。