[爆卦] 睽違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發現了一個六規則的圖靈機，其停機問題類似考拉茲猜想。

--

09/06 20:49