[爆卦] 睽違50年 科學家找到第五個忙碌海狸數

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://www.ptt.cc/bbs/Gossiping/M.1725626757.A.AFA.html