40年圖靈機(jī)難題被業(yè)余玩家攻破，陶哲軒：軟件輔助證明改變數(shù)學(xué)研究規(guī)則

AIGC動(dòng)態(tài)歡迎閱讀

原標(biāo)題：40年圖靈機(jī)難題被業(yè)余玩家攻破，陶哲軒：軟件輔助證明改變數(shù)學(xué)研究規(guī)則
關(guān)鍵字：圖靈機(jī),機(jī)器,規(guī)則,程序,貢獻(xiàn)者
文章來源：量子位
內(nèi)容字?jǐn)?shù)：0字

內(nèi)容摘要：

一水發(fā)自凹非寺量子位 | 公眾號 QbitAI40多年的計(jì)算機(jī)難題——忙碌海貍難題，被一群業(yè)余愛好者攻破了！
數(shù)學(xué)大佬陶哲軒轉(zhuǎn)發(fā)了這一消息，并欣慰表示：
這再一次體現(xiàn)了證明助手對于數(shù)學(xué)研究的協(xié)作是多么有用。
計(jì)算機(jī)科學(xué)家Scott Aaronson為此還寫了一篇博文，并大肆贊賞：
這個(gè)發(fā)現(xiàn)是自1983年以來，忙碌海貍函數(shù)研究中最重要的進(jìn)展。
具體而言，人們歷經(jīng)數(shù)十年努力，終于找到了第五個(gè)“忙碌海貍”圖靈機(jī)：
BB(5) =47,176,870（5狀態(tài)圖靈機(jī)，能在停下來之前寫下47,176,870個(gè)“1”）
圖靈機(jī)是一種抽象的計(jì)算模型，通過讀取和寫入0和1在無限磁帶上進(jìn)行計(jì)算。
早在40多年前，一群計(jì)算機(jī)科學(xué)家在德國多特蒙德舉行競賽，尋找“忙碌海貍”圖靈機(jī)。
找出一個(gè)特定的圖靈機(jī)，在它停止之前能夠?qū)懴伦疃嗟?（我們稱之為忙碌海貍數(shù)）。
通過找出特定狀態(tài)下能在停止前寫下最多1的圖靈機(jī)，我們能更好地理解計(jì)算理論的邊界。
自從1974年確定了第四個(gè)忙碌海貍數(shù)后，尋找第五個(gè)成了懸而未決的問題。
而現(xiàn)在，來自世界各地的20多名貢獻(xiàn)者（其中大多數(shù)人沒有傳統(tǒng)的學(xué)術(shù)資格），使用一款名為Coq證明助手

原文鏈接：40年圖靈機(jī)難題被業(yè)余玩家攻破，陶哲軒：軟件輔助證明改變數(shù)學(xué)研究規(guī)則