※ [本文转录自 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发现了一个六规则的图灵机 ，其停机问题类似考拉兹猜想。 --

※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 111.253.129.243 (台湾) ※ 文章网址: https://webptt.com/cn.aspx?n=bbs/Gossiping/M.1725626757.A.AFA.html ※ 编辑: jackliao1990 (111.253.129.243 台湾), 09/06/2024 20:52:57

※ 发信站: 批踢踢实业坊(ptt.cc) ※ 转录者: jackliao1990 (111.253.129.243 台湾), 09/06/2024 20:53:17