AIGC動態歡迎閱讀
原標題:40年圖靈機難題被業余玩家攻破,陶哲軒:軟件輔助證明改變數學研究規則
關鍵字:圖靈機,機器,規則,程序,貢獻者
文章來源:量子位
內容字數:0字
內容摘要:
一水 發自 凹非寺量子位 | 公眾號 QbitAI40多年的計算機難題——忙碌海貍難題,被一群業余愛好者攻破了!
數學大佬陶哲軒轉發了這一消息,并欣慰表示:
這再一次體現了證明助手對于數學研究的協作是多么有用。
計算機科學家Scott Aaronson為此還寫了一篇博文,并大肆贊賞:
這個發現是自1983年以來,忙碌海貍函數研究中最重要的進展。
具體而言,人們歷經數十年努力,終于找到了第五個“忙碌海貍”圖靈機:
BB(5) =47,176,870(5狀態圖靈機,能在停下來之前寫下47,176,870個“1”)
圖靈機是一種抽象的計算模型,通過讀取和寫入0和1在無限磁帶上進行計算。
早在40多年前,一群計算機科學家在德國多特蒙德舉行競賽,尋找“忙碌海貍”圖靈機。
找出一個特定的圖靈機,在它停止之前能夠寫下最多的1(我們稱之為忙碌海貍數)。
通過找出特定狀態下能在停止前寫下最多1的圖靈機,我們能更好地理解計算理論的邊界。
自從1974年確定了第四個忙碌海貍數后,尋找第五個成了懸而未決的問題。
而現在,來自世界各地的20多名貢獻者(其中大多數人沒有傳統的學術資格),使用一款名為Coq證明助手
原文鏈接:40年圖靈機難題被業余玩家攻破,陶哲軒:軟件輔助證明改變數學研究規則
聯系作者
文章來源:量子位
作者微信:
作者簡介:
? 版權聲明
文章版權歸作者所有,未經允許請勿轉載。
相關文章
暫無評論...